From 9b4008723a4cad0095107343dbe55bf4715ec994 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Thu, 25 Jul 2024 10:52:32 +0300 Subject: [PATCH 01/26] Auction manager initial setup --- certora/config/AuctionManager.conf | 20 ++++ certora/config/EETH.conf | 0 certora/specs/AuctionManager.spec | 181 +++++++++++++++++++++++++++++ certora/specs/EETH.spec | 43 +++++++ 4 files changed, 244 insertions(+) create mode 100644 certora/config/AuctionManager.conf create mode 100644 certora/config/EETH.conf create mode 100644 certora/specs/AuctionManager.spec create mode 100644 certora/specs/EETH.spec diff --git a/certora/config/AuctionManager.conf b/certora/config/AuctionManager.conf new file mode 100644 index 00000000..4530f2e5 --- /dev/null +++ b/certora/config/AuctionManager.conf @@ -0,0 +1,20 @@ +{ + "files": [ + "src/AuctionManager.sol", + "src/NodeOperatorManager.sol" + ], + "link": [ + "AuctionManager:nodeOperatorManager=NodeOperatorManager" + ], + "packages": [ + "@openzeppelin=lib/openzeppelin-contracts", + "forge-std=lib/forge-std/src" + ], + "verify": "AuctionManager:certora/specs/AuctionManager.spec", + "optimistic_loop": true, + "optimistic_fallback": true, + "loop_iter": "3", + "solc": "solc8.24", + "prover_args": ["-enableStorageSplitting false"], + "msg": "all AuctionManager", +} diff --git a/certora/config/EETH.conf b/certora/config/EETH.conf new file mode 100644 index 00000000..e69de29b diff --git a/certora/specs/AuctionManager.spec b/certora/specs/AuctionManager.spec new file mode 100644 index 00000000..9d3fa1da --- /dev/null +++ b/certora/specs/AuctionManager.spec @@ -0,0 +1,181 @@ +using NodeOperatorManager as NodeOperatorManager; +/* Verification of `AuctionManager` */ +methods { + + // Getters: + function whitelistEnabled() external returns (bool) envfree; + function whitelistBidAmount() external returns (uint128) envfree; + function minBidAmount() external returns (uint64) envfree; + function maxBidAmount() external returns (uint64) envfree; + function numberOfActiveBids() external returns (uint256) envfree; + function numberOfBids() external returns (uint256) envfree; + function bids(uint256) external returns (uint256, uint64, address, bool) envfree; + function getBidOwner(uint256) external returns (address) envfree; + function isBidActive(uint256) external returns (bool) envfree; + + + function NodeOperatorManager.getUserTotalKeys(address) external returns (uint64) envfree; + function NodeOperatorManager.getNumKeysRemaining(address) external returns (uint64) envfree; +} + +/// Is persistent because it mirrors the PoolManager storage. +persistent ghost mapping(uint256 => uint256) bids_amount { + init_state axiom forall uint256 bid_id . bids_amount[bid_id] == 0; +} + +ghost mathint sum_of_bids{ + init_state axiom sum_of_bids == 0; +} + +ghost mathint sum_of_active_bids { + init_state axiom sum_of_active_bids == 0; +} + +ghost mathint sum_of_all_bids_amounts; + +ghost mathint sum_of_all_active_bids_amounts; + +ghost uint256 latest_bid_id; + +// ghost mapping(uint256 => uint64) bids_keys_indexes { +// init_state axiom forall uint256 bid_id . bids_amount[bid_id] == 0; +// } + +// ghost mapping(address => uint256[]) user_bid_ids { +// init_state axiom forall address user . forall uint256 index . user_bid_ids[user][index] == 0; +// } + +ghost mapping(uint256 => bool) bids_is_active { + init_state axiom forall uint256 bid_id . bids_is_active[bid_id] == false; +} + +ghost mapping(address => uint256) user_last_bid_id_index { + init_state axiom forall address user . user_last_bid_id_index[user] == 0; +} + +hook Sstore bids[KEY uint256 bid_id].amount uint256 new_amount (uint256 old_amount) { + bids_amount[bid_id] = new_amount; + + // if (old_amount == 0) { // might not be necesary if bid amount is immutable. + sum_of_bids = sum_of_bids + 1; + sum_of_all_bids_amounts = sum_of_all_bids_amounts + new_amount; + + // user_bid_ids[user_last_bid_id_index[user]] = bid_id; + // user_last_bid_id_index[user] = user_last_bid_id_index[user] + 1; +} + +hook Sload uint256 _amount bids[KEY uint256 bid_id].amount { + require _amount == bids_amount[bid_id]; +} + +// ghost mapping(unit256 => bool) was_bid_activated { +// init_state axiom forall uint256 bid_id . was_bid_activated[bid_id] == false; +// } + +hook Sstore bids[KEY uint256 bid_id].isActive bool new_acitive (bool old_active) { + if (new_acitive && !old_active) { + sum_of_active_bids = sum_of_active_bids + 1; + sum_of_all_active_bids_amounts = sum_of_all_active_bids_amounts + bids_amount[bid_id]; + } else if (!new_acitive && old_active) { + sum_of_active_bids = sum_of_active_bids - 1; + sum_of_all_active_bids_amounts = sum_of_all_active_bids_amounts - bids_amount[bid_id]; + } + bids_is_active[bid_id] = new_acitive; +} + +hook Sload bool _isActive bids[KEY uint256 bid_id].isActive { + require _isActive == bids_is_active[bid_id]; +} + +// numberOfActiveBids equals the sum of active bids. +invariant numberOfActiveBidsCorrect() + sum_of_active_bids == to_mathint(numberOfActiveBids()); + +// numberOfBids equals the sum of all bids. +invariant numberOfBidsEqTheSumOfAllBids() + sum_of_bids == to_mathint(numberOfBids()); + +// the sum of all used keys equals num of bids. +// invariant numOfAllUsedKeysEqNumOfBids() {} + +// rule bidderPubKeyIndexIsUniqePerUser() {} + +// rule bidsAmountImmutable() {} + + +/// @title Functions filtered out since they use `delegatecall` +definition isFilteredFunc(method f) returns bool = ( + f.selector == sig:upgradeToAndCall(address, bytes).selector +); + + +/// @title The contact is set as initialized in the constructor -- seems a bug? +invariant alwaysInitialized() + currentContract._initialized > 0 + filtered {f -> !isFilteredFunc(f)} + +// rule manager_initialized_once() { +// env e; +// calldataarg args; + +// bool isInitializedBefore = currentContract._initialized; + +// // call initialize: + +// assert !isInitializedBefore && currentContract._initialized; +// } + +rule integrityOfCreateBid(uint256 _bidSize, uint256 _bidAmountPerBid) { + env e; + uint256 newBidId; + mathint msgValue = e.msg.value; + uint256[] bidArray; + mathint numberOfBidsBefore = numberOfBids(); + mathint numberOfActiveBidsBefore = numberOfActiveBids(); + mathint bidIndexInBatch = newBidId - numberOfBidsBefore; + mathint senderFirstKeyIndex = NodeOperatorManager.getUserTotalKeys(e.msg.sender) - NodeOperatorManager.getNumKeysRemaining(e.msg.sender); + + require to_mathint(newBidId) < numberOfBidsBefore + _bidSize; + require to_mathint(newBidId) >= numberOfBidsBefore; + + // new bid fields: + uint256 amount; + uint64 bidderPubKeyIndex; + address bidderAddress; + bool isActive; + + bidArray = createBid(e, _bidSize, _bidAmountPerBid); + + // get one of the new bids: + amount, bidderPubKeyIndex, bidderAddress, isActive = bids(e, newBidId); + + mathint numberOfBidsAfter = numberOfBids(); + mathint numberOfActiveBidsAfter = numberOfActiveBids(); + mathint senderLastKeyIndex = NodeOperatorManager.getUserTotalKeys(e.msg.sender) - NodeOperatorManager.getNumKeysRemaining(e.msg.sender); + + // trivial due to requires: + assert msgValue == _bidSize * _bidAmountPerBid, "function should have reverted"; + // number of bids update correctly + assert numberOfBidsAfter == numberOfBidsBefore + _bidSize, "ammount of bids updated incorrectly"; + assert numberOfActiveBidsAfter == numberOfActiveBidsBefore + _bidSize, "ammount of active bids updated incorrectly"; + assert senderLastKeyIndex == senderFirstKeyIndex + _bidSize, "amount of used keys updated incorrectly"; + // the right bids were added: + assert amount == _bidAmountPerBid; + assert bidderPubKeyIndex == assert_uint64(senderFirstKeyIndex + bidIndexInBatch); + assert bidderAddress == e.msg.sender; + assert isActive; +} + +// rule integrityOfCancelBid(uint256 bidId) { +// env e; +// } + +// rule onlyWhiteListCanBid() {} + +/// @title Verifies that all functions can be called +rule sanity(method f) { + env e; + calldataarg args; + f(e, args); + satisfy true; +} \ No newline at end of file diff --git a/certora/specs/EETH.spec b/certora/specs/EETH.spec new file mode 100644 index 00000000..381eedda --- /dev/null +++ b/certora/specs/EETH.spec @@ -0,0 +1,43 @@ +methods { + function totalShares() external returns (uint256) envfree; + function shares(address) external returns (uint256) envfree; +} + + +// It is better to use `mathint` since doesn't overflow or underflow +persistent ghost mathint sumOfShares { + // `init_state` determines the state after the constructor + init_state axiom sumOfShares == 0; +} + +ghost mapping(address => uint256) sharesGhost { + init_state axiom forall address user . sharesGhost[user] == 0; +} + + +hook Sstore shares[KEY address _user] uint256 newVal (uint256 oldVal) { + // Update the sum in every change + sumOfShares = sumOfShares + newVal - oldVal; + sharesGhost[_user] = newVal; +} + + +/// @title `totalShares` is the sum of all shares +invariant totalSharesIsSumOfShares() + to_mathint(totalShares()) == sumOfShares + filtered { + f -> f.selector != sig:upgradeToAndCall(address,bytes).selector + } + + +/// @title The sum of shares of two users is not greater than total shares +invariant sumOfTwo(address user1, address user2) + shares(user1) + shares(user2) <= sumOfShares + filtered { + f -> f.selector != sig:upgradeToAndCall(address,bytes).selector + } + { + preserved { + requireInvariant totalSharesIsSumOfShares(); + } + } \ No newline at end of file From f93dcfebc1284f04e6bc2f4cb2d3eb0bd19b0222 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Thu, 25 Jul 2024 17:47:44 +0300 Subject: [PATCH 02/26] auctionManager new rules --- certora/config/AuctionManager.conf | 1 - certora/config/StakingManager.conf | 15 +++++ certora/specs/AuctionManager.spec | 90 ++++++++++++++++-------------- certora/specs/StakingManager.spec | 13 +++++ 4 files changed, 76 insertions(+), 43 deletions(-) create mode 100644 certora/config/StakingManager.conf create mode 100644 certora/specs/StakingManager.spec diff --git a/certora/config/AuctionManager.conf b/certora/config/AuctionManager.conf index 4530f2e5..59921a12 100644 --- a/certora/config/AuctionManager.conf +++ b/certora/config/AuctionManager.conf @@ -15,6 +15,5 @@ "optimistic_fallback": true, "loop_iter": "3", "solc": "solc8.24", - "prover_args": ["-enableStorageSplitting false"], "msg": "all AuctionManager", } diff --git a/certora/config/StakingManager.conf b/certora/config/StakingManager.conf new file mode 100644 index 00000000..df30929d --- /dev/null +++ b/certora/config/StakingManager.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "src/StakingManager.sol", + ], + "packages": [ + "@openzeppelin=lib/openzeppelin-contracts", + "forge-std=lib/forge-std/src" + ], + "verify": "StakingManager:certora/specs/StakingManager.spec", + "optimistic_loop": true, + "optimistic_fallback": true, + "loop_iter": "3", + "solc": "solc8.24", + "msg": "all StakingManager", +} diff --git a/certora/specs/AuctionManager.spec b/certora/specs/AuctionManager.spec index 9d3fa1da..19f118dd 100644 --- a/certora/specs/AuctionManager.spec +++ b/certora/specs/AuctionManager.spec @@ -16,6 +16,9 @@ methods { function NodeOperatorManager.getUserTotalKeys(address) external returns (uint64) envfree; function NodeOperatorManager.getNumKeysRemaining(address) external returns (uint64) envfree; + + + function _.upgradeToAndCall(address,bytes) external => NONDET; } /// Is persistent because it mirrors the PoolManager storage. @@ -23,7 +26,7 @@ persistent ghost mapping(uint256 => uint256) bids_amount { init_state axiom forall uint256 bid_id . bids_amount[bid_id] == 0; } -ghost mathint sum_of_bids{ +ghost mathint sum_of_bids { init_state axiom sum_of_bids == 0; } @@ -31,20 +34,16 @@ ghost mathint sum_of_active_bids { init_state axiom sum_of_active_bids == 0; } -ghost mathint sum_of_all_bids_amounts; +ghost mathint sum_of_all_bids_amounts { + init_state axiom sum_of_all_bids_amounts == 0; +} -ghost mathint sum_of_all_active_bids_amounts; +ghost mathint sum_of_all_active_bids_amounts { + init_state axiom sum_of_all_active_bids_amounts == 0; +} ghost uint256 latest_bid_id; -// ghost mapping(uint256 => uint64) bids_keys_indexes { -// init_state axiom forall uint256 bid_id . bids_amount[bid_id] == 0; -// } - -// ghost mapping(address => uint256[]) user_bid_ids { -// init_state axiom forall address user . forall uint256 index . user_bid_ids[user][index] == 0; -// } - ghost mapping(uint256 => bool) bids_is_active { init_state axiom forall uint256 bid_id . bids_is_active[bid_id] == false; } @@ -55,25 +54,16 @@ ghost mapping(address => uint256) user_last_bid_id_index { hook Sstore bids[KEY uint256 bid_id].amount uint256 new_amount (uint256 old_amount) { bids_amount[bid_id] = new_amount; - - // if (old_amount == 0) { // might not be necesary if bid amount is immutable. sum_of_bids = sum_of_bids + 1; sum_of_all_bids_amounts = sum_of_all_bids_amounts + new_amount; - - // user_bid_ids[user_last_bid_id_index[user]] = bid_id; - // user_last_bid_id_index[user] = user_last_bid_id_index[user] + 1; } hook Sload uint256 _amount bids[KEY uint256 bid_id].amount { require _amount == bids_amount[bid_id]; } -// ghost mapping(unit256 => bool) was_bid_activated { -// init_state axiom forall uint256 bid_id . was_bid_activated[bid_id] == false; -// } - hook Sstore bids[KEY uint256 bid_id].isActive bool new_acitive (bool old_active) { - if (new_acitive && !old_active) { + if (new_acitive) { sum_of_active_bids = sum_of_active_bids + 1; sum_of_all_active_bids_amounts = sum_of_all_active_bids_amounts + bids_amount[bid_id]; } else if (!new_acitive && old_active) { @@ -87,49 +77,65 @@ hook Sload bool _isActive bids[KEY uint256 bid_id].isActive { require _isActive == bids_is_active[bid_id]; } +// Functions filtered out since they use `delegatecall`. +definition isFilteredFunc(method f) returns bool = ( + f.selector == sig:upgradeToAndCall(address, bytes).selector +); + // numberOfActiveBids equals the sum of active bids. invariant numberOfActiveBidsCorrect() - sum_of_active_bids == to_mathint(numberOfActiveBids()); + sum_of_active_bids == to_mathint(numberOfActiveBids()) + filtered {f -> !isFilteredFunc(f)} // numberOfBids equals the sum of all bids. invariant numberOfBidsEqTheSumOfAllBids() - sum_of_bids == to_mathint(numberOfBids()); + sum_of_bids == to_mathint(numberOfBids()) + filtered {f -> !isFilteredFunc(f)} + +// solvency invariant - contract should hold atleast sumOfAllActiveBidAmounts amount of eth. +invariant activeBidsSolvency() + to_mathint(nativeBalances[currentContract]) >= sum_of_all_active_bids_amounts + filtered {f -> !isFilteredFunc(f)} // the sum of all used keys equals num of bids. // invariant numOfAllUsedKeysEqNumOfBids() {} +// chack for all bids to see if the key index is unique per user. // rule bidderPubKeyIndexIsUniqePerUser() {} -// rule bidsAmountImmutable() {} +rule bidImmutability(method f, uint256 bid_id) filtered {f -> !isFilteredFunc(f)} { + env e; + calldataarg args; + require bid_id < numberOfBids(); -/// @title Functions filtered out since they use `delegatecall` -definition isFilteredFunc(method f) returns bool = ( - f.selector == sig:upgradeToAndCall(address, bytes).selector -); + uint256 AmountBefore; + uint64 bidderPubKeyIndexBefore; + address bidderAddressBefore; + uint256 AmountAfter; + uint64 bidderPubKeyIndexAfter; + address bidderAddressAfter; + AmountBefore, bidderPubKeyIndexBefore, bidderAddressBefore, _ = bids(bid_id); -/// @title The contact is set as initialized in the constructor -- seems a bug? -invariant alwaysInitialized() - currentContract._initialized > 0 - filtered {f -> !isFilteredFunc(f)} - -// rule manager_initialized_once() { -// env e; -// calldataarg args; + f(e, args); -// bool isInitializedBefore = currentContract._initialized; + AmountAfter, bidderPubKeyIndexAfter, bidderAddressAfter, _ = bids(bid_id); -// // call initialize: + assert AmountBefore == AmountAfter, "bid amount was changed"; + assert bidderPubKeyIndexBefore == bidderPubKeyIndexAfter, "bidder key index was changed"; + assert bidderAddressBefore == bidderAddressAfter, "bidder address was changed"; +} -// assert !isInitializedBefore && currentContract._initialized; -// } +/// @title The contact is set as initialized in the constructor -- seems a bug? +invariant alwaysInitialized() + currentContract._initialized == max_uint8 + filtered {f -> !isFilteredFunc(f)} rule integrityOfCreateBid(uint256 _bidSize, uint256 _bidAmountPerBid) { env e; uint256 newBidId; mathint msgValue = e.msg.value; - uint256[] bidArray; mathint numberOfBidsBefore = numberOfBids(); mathint numberOfActiveBidsBefore = numberOfActiveBids(); mathint bidIndexInBatch = newBidId - numberOfBidsBefore; @@ -144,7 +150,7 @@ rule integrityOfCreateBid(uint256 _bidSize, uint256 _bidAmountPerBid) { address bidderAddress; bool isActive; - bidArray = createBid(e, _bidSize, _bidAmountPerBid); + createBid(e, _bidSize, _bidAmountPerBid); // get one of the new bids: amount, bidderPubKeyIndex, bidderAddress, isActive = bids(e, newBidId); diff --git a/certora/specs/StakingManager.spec b/certora/specs/StakingManager.spec new file mode 100644 index 00000000..bc34314f --- /dev/null +++ b/certora/specs/StakingManager.spec @@ -0,0 +1,13 @@ +// using NodeOperatorManager as NodeOperatorManager; +/* Verification of `AuctionManager` */ +methods { + function _.upgradeToAndCall(address,bytes) external => NONDET; +} + +/// @title Verifies that all functions can be called +rule sanity(method f) { + env e; + calldataarg args; + f(e, args); + satisfy true; +} \ No newline at end of file From 6ca9193b821537f75f986be3d337b99839bf56a0 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Sun, 28 Jul 2024 16:08:06 +0300 Subject: [PATCH 03/26] add eeth and weeth --- certora/config/EETH.conf | 18 +++++ certora/config/WeETH.conf | 18 +++++ certora/specs/EETH.spec | 123 ++++++++++++++++++++++++++++- certora/specs/WeETH.spec | 159 ++++++++++++++++++++++++++++++++++++++ 4 files changed, 315 insertions(+), 3 deletions(-) create mode 100644 certora/config/WeETH.conf create mode 100644 certora/specs/WeETH.spec diff --git a/certora/config/EETH.conf b/certora/config/EETH.conf index e69de29b..38719402 100644 --- a/certora/config/EETH.conf +++ b/certora/config/EETH.conf @@ -0,0 +1,18 @@ +{ + "files": [ + "src/EETH.sol" + ], + "link": [ + ], + "packages": [ + "@openzeppelin=lib/openzeppelin-contracts", + "forge-std=lib/forge-std/src" + ], + "verify": "EETH:certora/specs/EETH.spec", + "parametric_contracts": ["EETH"], + "optimistic_loop": true, + "optimistic_fallback": true, + "loop_iter": "3", + "solc": "solc8.24", + "msg": "EETH setup" +} \ No newline at end of file diff --git a/certora/config/WeETH.conf b/certora/config/WeETH.conf new file mode 100644 index 00000000..bde1e483 --- /dev/null +++ b/certora/config/WeETH.conf @@ -0,0 +1,18 @@ +{ + "files": [ + "src/WeETH.sol" + ], + "link": [ + ], + "packages": [ + "@openzeppelin=lib/openzeppelin-contracts", + "forge-std=lib/forge-std/src" + ], + "verify": "EETH:certora/specs/WeETH.spec", + "parametric_contracts": ["WeETH"], + "optimistic_loop": true, + "optimistic_fallback": true, + "loop_iter": "3", + "solc": "solc8.24", + "msg": "EETH setup" +} \ No newline at end of file diff --git a/certora/specs/EETH.spec b/certora/specs/EETH.spec index 381eedda..c89fbe0c 100644 --- a/certora/specs/EETH.spec +++ b/certora/specs/EETH.spec @@ -1,8 +1,15 @@ methods { function totalShares() external returns (uint256) envfree; function shares(address) external returns (uint256) envfree; + function allowance(address, address) external returns (uint256) envfree; + + function _.sharesForAmount(uint256 amount) external => identity(amount) expect uint256; + function _.amountForShare(uint256 amount) external => identity(amount) expect uint256; } +function identity(uint256 x) returns uint256 { + return x; +} // It is better to use `mathint` since doesn't overflow or underflow persistent ghost mathint sumOfShares { @@ -21,6 +28,9 @@ hook Sstore shares[KEY address _user] uint256 newVal (uint256 oldVal) { sharesGhost[_user] = newVal; } +hook Sload uint256 _shares shares[KEY address _user] { + require _shares == sharesGhost[_user]; +} /// @title `totalShares` is the sum of all shares invariant totalSharesIsSumOfShares() @@ -29,15 +39,122 @@ invariant totalSharesIsSumOfShares() f -> f.selector != sig:upgradeToAndCall(address,bytes).selector } - /// @title The sum of shares of two users is not greater than total shares invariant sumOfTwo(address user1, address user2) shares(user1) + shares(user2) <= sumOfShares filtered { f -> f.selector != sig:upgradeToAndCall(address,bytes).selector - } + } { preserved { requireInvariant totalSharesIsSumOfShares(); } - } \ No newline at end of file + } + +/** +Verify that there is no fee on transfer. +**/ +rule noFeeOnTransfer(address bob, uint256 amount) { + env e; + require bob != e.msg.sender; + uint256 balanceSenderBefore = shares(e.msg.sender); + uint256 balanceBefore = shares(bob); + + transfer(e, bob, amount); + + uint256 balanceAfter = shares(bob); + uint256 balanceSenderAfter = shares(e.msg.sender); + assert balanceAfter == assert_uint256(balanceBefore + amount); + assert balanceSenderAfter == assert_uint256(balanceSenderBefore - amount); +} + +/** +Token transfer works correctly. Balances are updated if not reverted. +If reverted then the transfer amount was too high, or the recipient either 0, the same as the sender or the currentContract. +**/ +rule transferCorrect(address to, uint256 amount) { + env e; + require e.msg.value == 0 && e.msg.sender != 0; + uint256 fromBalanceBefore = shares(e.msg.sender); + uint256 toBalanceBefore = shares(to); + require fromBalanceBefore + toBalanceBefore <= max_uint256; + + transfer@withrevert(e, to, amount); + bool reverted = lastReverted; + if (!reverted) { + if (e.msg.sender == to) { + assert shares(e.msg.sender) == fromBalanceBefore; + } else { + assert shares(e.msg.sender) == assert_uint256(fromBalanceBefore - amount); + assert shares(to) == assert_uint256(toBalanceBefore + amount); + } + } else { + assert amount > fromBalanceBefore || to == 0 || e.msg.sender == to; + } +} + +/** +Test that transferFrom works correctly. Balances are updated if not reverted. +**/ +rule transferFromCorrect(address from, address to, uint256 amount) { + env e; + require e.msg.value == 0; + uint256 fromBalanceBefore = shares(from); + uint256 toBalanceBefore = shares(to); + uint256 allowanceBefore = allowance(from, e.msg.sender); + require fromBalanceBefore + toBalanceBefore <= max_uint256; + + transferFrom(e, from, to, amount); + + assert from != to => + shares(from) == assert_uint256(fromBalanceBefore - amount) && + shares(to) == assert_uint256(toBalanceBefore + amount); +} + +/** +transferFrom should revert if and only if the amount is too high or the recipient is 0 or the contract itself. +**/ +rule transferFromReverts(address from, address to, uint256 amount) { + env e; + uint256 allowanceBefore = allowance(from, e.msg.sender); + uint256 fromBalanceBefore = shares(from); + require from != 0 && e.msg.sender != 0; + require e.msg.value == 0; + require fromBalanceBefore + shares(to) <= max_uint256; + + transferFrom@withrevert(e, from, to, amount); + + assert lastReverted <=> (allowanceBefore < amount || amount > fromBalanceBefore || to == 0); +} + +/** +Transfer from msg.sender to recipient doesn't change the balance of other addresses. +**/ +rule TransferDoesntChangeOtherBalance(address to, uint256 amount, address other) { + env e; + require other != e.msg.sender; + require other != to && other != currentContract; + uint256 balanceBefore = shares(other); + transfer(e, to, amount); + assert balanceBefore == shares(other); +} + +/** +Transfer from sender to recipient using transferFrom doesn't change the balance of other addresses. +**/ +rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amount, address other) { + env e; + require other != from; + require other != to; + uint256 balanceBefore = shares(other); + transferFrom(e, from, to, amount); + assert balanceBefore == shares(other); +} + +// rule mintMonotonicity() {} + +// rule mintAccumulativity() {} + +// rule burnMonotonicity() {} + +// rule burnAccumulativity() {} diff --git a/certora/specs/WeETH.spec b/certora/specs/WeETH.spec new file mode 100644 index 00000000..4dfedc18 --- /dev/null +++ b/certora/specs/WeETH.spec @@ -0,0 +1,159 @@ +methods { + function totalShares() external returns (uint256) envfree; + function shares(address) external returns (uint256) envfree; + function allowance(address, address) external returns (uint256) envfree; + + function _.sharesForAmount(uint256 amount) external => identity(amount) expect uint256; +} + +function identity(uint256 x) returns uint256 { + return x; +} + +// It is better to use `mathint` since doesn't overflow or underflow +persistent ghost mathint sumOfShares { + // `init_state` determines the state after the constructor + init_state axiom sumOfShares == 0; +} + +ghost mapping(address => uint256) sharesGhost { + init_state axiom forall address user . sharesGhost[user] == 0; +} + + +hook Sstore shares[KEY address _user] uint256 newVal (uint256 oldVal) { + // Update the sum in every change + sumOfShares = sumOfShares + newVal - oldVal; + sharesGhost[_user] = newVal; +} + +hook Sload uint256 _shares shares[KEY address _user] { + require _shares == sharesGhost[_user]; +} + +/// @title `totalShares` is the sum of all shares +invariant totalSharesIsSumOfShares() + to_mathint(totalShares()) == sumOfShares + filtered { + f -> f.selector != sig:upgradeToAndCall(address,bytes).selector + } + +/// @title The sum of shares of two users is not greater than total shares +invariant sumOfTwo(address user1, address user2) + shares(user1) + shares(user2) <= sumOfShares + filtered { + f -> f.selector != sig:upgradeToAndCall(address,bytes).selector + } + { + preserved { + requireInvariant totalSharesIsSumOfShares(); + } + } + +/** +Verify that there is no fee on transfer. +**/ +rule noFeeOnTransfer(address bob, uint256 amount) { + env e; + require bob != e.msg.sender; + uint256 balanceSenderBefore = shares(e.msg.sender); + uint256 balanceBefore = shares(bob); + + transfer(e, bob, amount); + + uint256 balanceAfter = shares(bob); + uint256 balanceSenderAfter = shares(e.msg.sender); + assert balanceAfter == assert_uint256(balanceBefore + amount); + assert balanceSenderAfter == assert_uint256(balanceSenderBefore - amount); +} + +/** +Token transfer works correctly. Balances are updated if not reverted. +If reverted then the transfer amount was too high, or the recipient either 0, the same as the sender or the currentContract. +**/ +rule transferCorrect(address to, uint256 amount) { + env e; + require e.msg.value == 0 && e.msg.sender != 0; + uint256 fromBalanceBefore = shares(e.msg.sender); + uint256 toBalanceBefore = shares(to); + require fromBalanceBefore + toBalanceBefore <= max_uint256; + + transfer@withrevert(e, to, amount); + bool reverted = lastReverted; + if (!reverted) { + if (e.msg.sender == to) { + assert shares(e.msg.sender) == fromBalanceBefore; + } else { + assert shares(e.msg.sender) == assert_uint256(fromBalanceBefore - amount); + assert shares(to) == assert_uint256(toBalanceBefore + amount); + } + } else { + assert amount > fromBalanceBefore || to == 0 || e.msg.sender == to || to == currentContract; + } +} + +/** +Test that transferFrom works correctly. Balances are updated if not reverted. +**/ +rule transferFromCorrect(address from, address to, uint256 amount) { + env e; + require e.msg.value == 0; + uint256 fromBalanceBefore = shares(from); + uint256 toBalanceBefore = shares(to); + uint256 allowanceBefore = allowance(from, e.msg.sender); + require fromBalanceBefore + toBalanceBefore <= max_uint256; + + transferFrom(e, from, to, amount); + + assert from != to => + shares(from) == assert_uint256(fromBalanceBefore - amount) && + shares(to) == assert_uint256(toBalanceBefore + amount); +} + +/** +transferFrom should revert if and only if the amount is too high or the recipient is 0 or the contract itself. +**/ +rule transferFromReverts(address from, address to, uint256 amount) { + env e; + uint256 allowanceBefore = allowance(from, e.msg.sender); + uint256 fromBalanceBefore = shares(from); + require from != 0 && e.msg.sender != 0; + require e.msg.value == 0; + require fromBalanceBefore + shares(to) <= max_uint256; + + transferFrom@withrevert(e, from, to, amount); + + assert lastReverted <=> (allowanceBefore < amount || amount > fromBalanceBefore || to == 0 || to == currentContract); +} + +/** +Transfer from msg.sender to recipient doesn't change the balance of other addresses. +**/ +rule TransferDoesntChangeOtherBalance(address to, uint256 amount, address other) { + env e; + require other != e.msg.sender; + require other != to && other != currentContract; + uint256 balanceBefore = shares(other); + transfer(e, to, amount); + assert balanceBefore == shares(other); +} + +/** +Transfer from sender to recipient using transferFrom doesn't change the balance of other addresses. +**/ +rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amount, address other) { + env e; + require other != from; + require other != to; + uint256 balanceBefore = shares(other); + transferFrom(e, from, to, amount); + assert balanceBefore == shares(other); +} + +// rule mintMonotonicity() {} + +// rule mintAccumulativity() {} + +// rule burnMonotonicity() {} + +// rule burnAccumulativity() {} From 576f37d2fe5095f27fb4941c2902dfd7398f2e80 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Sun, 28 Jul 2024 16:21:46 +0300 Subject: [PATCH 04/26] update weeth spec --- certora/specs/WeETH.spec | 158 ++------------------------------------- 1 file changed, 8 insertions(+), 150 deletions(-) diff --git a/certora/specs/WeETH.spec b/certora/specs/WeETH.spec index 4dfedc18..f84b63a9 100644 --- a/certora/specs/WeETH.spec +++ b/certora/specs/WeETH.spec @@ -1,159 +1,17 @@ methods { - function totalShares() external returns (uint256) envfree; - function shares(address) external returns (uint256) envfree; - function allowance(address, address) external returns (uint256) envfree; + function wrap(uint256) external returns (uint256); + function wrapWithPermit(uint256, ILiquidityPool.PermitInput) external returns (uint256); + function unwrap(uint256) external returns (uint256); + function rescueTreasuryWeeth() external; + function getWeETHByeETH(uint256) external returns (uint256) envfree; + function getEETHByWeETH(uint256) external returns (uint256) envfree; + function getRate() external returns (uint256) envfree; function _.sharesForAmount(uint256 amount) external => identity(amount) expect uint256; + function _.amountForShare(uint256 amount) external => identity(amount) expect uint256; } function identity(uint256 x) returns uint256 { return x; } -// It is better to use `mathint` since doesn't overflow or underflow -persistent ghost mathint sumOfShares { - // `init_state` determines the state after the constructor - init_state axiom sumOfShares == 0; -} - -ghost mapping(address => uint256) sharesGhost { - init_state axiom forall address user . sharesGhost[user] == 0; -} - - -hook Sstore shares[KEY address _user] uint256 newVal (uint256 oldVal) { - // Update the sum in every change - sumOfShares = sumOfShares + newVal - oldVal; - sharesGhost[_user] = newVal; -} - -hook Sload uint256 _shares shares[KEY address _user] { - require _shares == sharesGhost[_user]; -} - -/// @title `totalShares` is the sum of all shares -invariant totalSharesIsSumOfShares() - to_mathint(totalShares()) == sumOfShares - filtered { - f -> f.selector != sig:upgradeToAndCall(address,bytes).selector - } - -/// @title The sum of shares of two users is not greater than total shares -invariant sumOfTwo(address user1, address user2) - shares(user1) + shares(user2) <= sumOfShares - filtered { - f -> f.selector != sig:upgradeToAndCall(address,bytes).selector - } - { - preserved { - requireInvariant totalSharesIsSumOfShares(); - } - } - -/** -Verify that there is no fee on transfer. -**/ -rule noFeeOnTransfer(address bob, uint256 amount) { - env e; - require bob != e.msg.sender; - uint256 balanceSenderBefore = shares(e.msg.sender); - uint256 balanceBefore = shares(bob); - - transfer(e, bob, amount); - - uint256 balanceAfter = shares(bob); - uint256 balanceSenderAfter = shares(e.msg.sender); - assert balanceAfter == assert_uint256(balanceBefore + amount); - assert balanceSenderAfter == assert_uint256(balanceSenderBefore - amount); -} - -/** -Token transfer works correctly. Balances are updated if not reverted. -If reverted then the transfer amount was too high, or the recipient either 0, the same as the sender or the currentContract. -**/ -rule transferCorrect(address to, uint256 amount) { - env e; - require e.msg.value == 0 && e.msg.sender != 0; - uint256 fromBalanceBefore = shares(e.msg.sender); - uint256 toBalanceBefore = shares(to); - require fromBalanceBefore + toBalanceBefore <= max_uint256; - - transfer@withrevert(e, to, amount); - bool reverted = lastReverted; - if (!reverted) { - if (e.msg.sender == to) { - assert shares(e.msg.sender) == fromBalanceBefore; - } else { - assert shares(e.msg.sender) == assert_uint256(fromBalanceBefore - amount); - assert shares(to) == assert_uint256(toBalanceBefore + amount); - } - } else { - assert amount > fromBalanceBefore || to == 0 || e.msg.sender == to || to == currentContract; - } -} - -/** -Test that transferFrom works correctly. Balances are updated if not reverted. -**/ -rule transferFromCorrect(address from, address to, uint256 amount) { - env e; - require e.msg.value == 0; - uint256 fromBalanceBefore = shares(from); - uint256 toBalanceBefore = shares(to); - uint256 allowanceBefore = allowance(from, e.msg.sender); - require fromBalanceBefore + toBalanceBefore <= max_uint256; - - transferFrom(e, from, to, amount); - - assert from != to => - shares(from) == assert_uint256(fromBalanceBefore - amount) && - shares(to) == assert_uint256(toBalanceBefore + amount); -} - -/** -transferFrom should revert if and only if the amount is too high or the recipient is 0 or the contract itself. -**/ -rule transferFromReverts(address from, address to, uint256 amount) { - env e; - uint256 allowanceBefore = allowance(from, e.msg.sender); - uint256 fromBalanceBefore = shares(from); - require from != 0 && e.msg.sender != 0; - require e.msg.value == 0; - require fromBalanceBefore + shares(to) <= max_uint256; - - transferFrom@withrevert(e, from, to, amount); - - assert lastReverted <=> (allowanceBefore < amount || amount > fromBalanceBefore || to == 0 || to == currentContract); -} - -/** -Transfer from msg.sender to recipient doesn't change the balance of other addresses. -**/ -rule TransferDoesntChangeOtherBalance(address to, uint256 amount, address other) { - env e; - require other != e.msg.sender; - require other != to && other != currentContract; - uint256 balanceBefore = shares(other); - transfer(e, to, amount); - assert balanceBefore == shares(other); -} - -/** -Transfer from sender to recipient using transferFrom doesn't change the balance of other addresses. -**/ -rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amount, address other) { - env e; - require other != from; - require other != to; - uint256 balanceBefore = shares(other); - transferFrom(e, from, to, amount); - assert balanceBefore == shares(other); -} - -// rule mintMonotonicity() {} - -// rule mintAccumulativity() {} - -// rule burnMonotonicity() {} - -// rule burnAccumulativity() {} From 07577f926dc0f0bf20a4fe0d9baebc4171a69b72 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Sun, 28 Jul 2024 17:26:38 +0300 Subject: [PATCH 05/26] update weeth --- certora/config/WeETH.conf | 6 ++++-- certora/specs/WeETH.spec | 8 ++++++++ 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/certora/config/WeETH.conf b/certora/config/WeETH.conf index bde1e483..98d7d948 100644 --- a/certora/config/WeETH.conf +++ b/certora/config/WeETH.conf @@ -1,14 +1,16 @@ { "files": [ - "src/WeETH.sol" + "src/WeETH.sol", + "src/EETH.sol" ], "link": [ + "WeETH:eETH=EETH" ], "packages": [ "@openzeppelin=lib/openzeppelin-contracts", "forge-std=lib/forge-std/src" ], - "verify": "EETH:certora/specs/WeETH.spec", + "verify": "WeETH:certora/specs/WeETH.spec", "parametric_contracts": ["WeETH"], "optimistic_loop": true, "optimistic_fallback": true, diff --git a/certora/specs/WeETH.spec b/certora/specs/WeETH.spec index f84b63a9..49e03389 100644 --- a/certora/specs/WeETH.spec +++ b/certora/specs/WeETH.spec @@ -15,3 +15,11 @@ function identity(uint256 x) returns uint256 { return x; } +rule sanity(method f) { + env e; + calldataarg args; + + f(e,args); + + assert false; +} From dddb740363033a9b717459bb3349ac3043a320c9 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Sun, 28 Jul 2024 17:28:17 +0300 Subject: [PATCH 06/26] . --- certora/specs/WeETH.spec | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/certora/specs/WeETH.spec b/certora/specs/WeETH.spec index 49e03389..25308527 100644 --- a/certora/specs/WeETH.spec +++ b/certora/specs/WeETH.spec @@ -16,10 +16,8 @@ function identity(uint256 x) returns uint256 { } rule sanity(method f) { - env e; + env e; calldataarg args; - - f(e,args); - - assert false; + f(e, args); + satisfy true; } From fcbef3970165104a9267fad4d302722c24a88c3d Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Sun, 4 Aug 2024 16:32:02 +0300 Subject: [PATCH 07/26] update setups - stakingManager --- certora/config/StakingManager.conf | 8 ++ certora/specs/AuctionManageSetup.spec | 59 ++++++++++++++ certora/specs/AuctionManager.spec | 62 +-------------- certora/specs/BNFT.spec | 20 +++++ certora/specs/StakingManager.spec | 107 ++++++++++++++++++++++++-- certora/specs/TNFT.spec | 20 +++++ 6 files changed, 209 insertions(+), 67 deletions(-) create mode 100644 certora/specs/AuctionManageSetup.spec create mode 100644 certora/specs/BNFT.spec create mode 100644 certora/specs/TNFT.spec diff --git a/certora/config/StakingManager.conf b/certora/config/StakingManager.conf index df30929d..790a1d92 100644 --- a/certora/config/StakingManager.conf +++ b/certora/config/StakingManager.conf @@ -1,6 +1,14 @@ { "files": [ "src/StakingManager.sol", + "src/AuctionManager.sol", + "src/NodeOperatorManager.sol", + "src/TNFT.sol", + "src/BNFT.sol", + ], + "link": [ + "StakingManager:auctionManager=AuctionManager", + "AuctionManager:nodeOperatorManager=NodeOperatorManager", ], "packages": [ "@openzeppelin=lib/openzeppelin-contracts", diff --git a/certora/specs/AuctionManageSetup.spec b/certora/specs/AuctionManageSetup.spec new file mode 100644 index 00000000..1751ac90 --- /dev/null +++ b/certora/specs/AuctionManageSetup.spec @@ -0,0 +1,59 @@ +methods { + function _.upgradeToAndCall(address,bytes) external => NONDET; +} + +/// Is persistent because it mirrors the PoolManager storage. +persistent ghost mapping(uint256 => uint256) bids_amount { + init_state axiom forall uint256 bid_id . bids_amount[bid_id] == 0; +} + +ghost mathint sum_of_bids { + init_state axiom sum_of_bids == 0; +} + +ghost mathint sum_of_active_bids { + init_state axiom sum_of_active_bids == 0; +} + +ghost mathint sum_of_all_bids_amounts { + init_state axiom sum_of_all_bids_amounts == 0; +} + +ghost mathint sum_of_all_active_bids_amounts { + init_state axiom sum_of_all_active_bids_amounts == 0; +} + +ghost uint256 latest_bid_id; + +ghost mapping(uint256 => bool) bids_is_active { + init_state axiom forall uint256 bid_id . bids_is_active[bid_id] == false; +} + +ghost mapping(address => uint256) user_last_bid_id_index { + init_state axiom forall address user . user_last_bid_id_index[user] == 0; +} + +hook Sstore bids[KEY uint256 bid_id].amount uint256 new_amount (uint256 old_amount) { + bids_amount[bid_id] = new_amount; + sum_of_bids = sum_of_bids + 1; + sum_of_all_bids_amounts = sum_of_all_bids_amounts + new_amount; +} + +hook Sload uint256 _amount bids[KEY uint256 bid_id].amount { + require _amount == bids_amount[bid_id]; +} + +hook Sstore bids[KEY uint256 bid_id].isActive bool new_acitive (bool old_active) { + if (new_acitive) { + sum_of_active_bids = sum_of_active_bids + 1; + sum_of_all_active_bids_amounts = sum_of_all_active_bids_amounts + bids_amount[bid_id]; + } else if (!new_acitive && old_active) { + sum_of_active_bids = sum_of_active_bids - 1; + sum_of_all_active_bids_amounts = sum_of_all_active_bids_amounts - bids_amount[bid_id]; + } + bids_is_active[bid_id] = new_acitive; +} + +hook Sload bool _isActive bids[KEY uint256 bid_id].isActive { + require _isActive == bids_is_active[bid_id]; +} diff --git a/certora/specs/AuctionManager.spec b/certora/specs/AuctionManager.spec index 19f118dd..0ace7ea9 100644 --- a/certora/specs/AuctionManager.spec +++ b/certora/specs/AuctionManager.spec @@ -1,3 +1,5 @@ +import "./AuctionManageSetup.spec"; + using NodeOperatorManager as NodeOperatorManager; /* Verification of `AuctionManager` */ methods { @@ -13,68 +15,8 @@ methods { function getBidOwner(uint256) external returns (address) envfree; function isBidActive(uint256) external returns (bool) envfree; - function NodeOperatorManager.getUserTotalKeys(address) external returns (uint64) envfree; function NodeOperatorManager.getNumKeysRemaining(address) external returns (uint64) envfree; - - - function _.upgradeToAndCall(address,bytes) external => NONDET; -} - -/// Is persistent because it mirrors the PoolManager storage. -persistent ghost mapping(uint256 => uint256) bids_amount { - init_state axiom forall uint256 bid_id . bids_amount[bid_id] == 0; -} - -ghost mathint sum_of_bids { - init_state axiom sum_of_bids == 0; -} - -ghost mathint sum_of_active_bids { - init_state axiom sum_of_active_bids == 0; -} - -ghost mathint sum_of_all_bids_amounts { - init_state axiom sum_of_all_bids_amounts == 0; -} - -ghost mathint sum_of_all_active_bids_amounts { - init_state axiom sum_of_all_active_bids_amounts == 0; -} - -ghost uint256 latest_bid_id; - -ghost mapping(uint256 => bool) bids_is_active { - init_state axiom forall uint256 bid_id . bids_is_active[bid_id] == false; -} - -ghost mapping(address => uint256) user_last_bid_id_index { - init_state axiom forall address user . user_last_bid_id_index[user] == 0; -} - -hook Sstore bids[KEY uint256 bid_id].amount uint256 new_amount (uint256 old_amount) { - bids_amount[bid_id] = new_amount; - sum_of_bids = sum_of_bids + 1; - sum_of_all_bids_amounts = sum_of_all_bids_amounts + new_amount; -} - -hook Sload uint256 _amount bids[KEY uint256 bid_id].amount { - require _amount == bids_amount[bid_id]; -} - -hook Sstore bids[KEY uint256 bid_id].isActive bool new_acitive (bool old_active) { - if (new_acitive) { - sum_of_active_bids = sum_of_active_bids + 1; - sum_of_all_active_bids_amounts = sum_of_all_active_bids_amounts + bids_amount[bid_id]; - } else if (!new_acitive && old_active) { - sum_of_active_bids = sum_of_active_bids - 1; - sum_of_all_active_bids_amounts = sum_of_all_active_bids_amounts - bids_amount[bid_id]; - } - bids_is_active[bid_id] = new_acitive; -} - -hook Sload bool _isActive bids[KEY uint256 bid_id].isActive { - require _isActive == bids_is_active[bid_id]; } // Functions filtered out since they use `delegatecall`. diff --git a/certora/specs/BNFT.spec b/certora/specs/BNFT.spec new file mode 100644 index 00000000..4b84375b --- /dev/null +++ b/certora/specs/BNFT.spec @@ -0,0 +1,20 @@ +methods { + // IERC721Upgradeable: + function balanceOf(address) external returns (uint256) envfree; + function ownerOf(uint256) external returns (address) envfree; + function safeTransferFrom(address, address, uint256, bytes) external; + function safeTransferFrom(address, address, uint256) external; + function transferFrom(address, address, uint256) external; + function approve(address, uint256) external; + function setApprovalForAll(address, bool) external; + function getApproved(uint256 tokenId) external view returns (address operator); + function isApprovedForAll(address, address) external returns (bool) envfree; + + // BNFT: + function burnFromWithdrawal(uint256) external; + function initialize() external; + function initializeOnUpgrade(address) external; + function mint(address, uint256) external; + function burnFromCancelBNftFlow(uint256) external; + function upgradeTo(address) external; +} diff --git a/certora/specs/StakingManager.spec b/certora/specs/StakingManager.spec index bc34314f..01ada430 100644 --- a/certora/specs/StakingManager.spec +++ b/certora/specs/StakingManager.spec @@ -1,13 +1,106 @@ -// using NodeOperatorManager as NodeOperatorManager; -/* Verification of `AuctionManager` */ +using AuctionManager as auctionManager; methods { + // Getters: + function maxBatchDepositSize() external returns (uint128) envfree; + function stakeAmount() external returns (uint128) envfree; + function liquidityPoolContract() external returns (address) envfree; + function bidIdToStakerInfo(uint256) external returns (address, bytes1, bytes10) envfree; + + function initialize(address, address) external; + function initializeOnUpgrade(address, address) external; + function batchDepositWithBidIds(uint256[], uint256, address, address, address, bool, uint256) external returns (uint256[] memory); + function batchCancelDeposit(uint256[], address) external; + function batchRegisterValidators(uint256[], address, address, IStakingManager.DepositData[], address) external; + function batchApproveRegistration(uint256[], bytes[], bytes[], bytes32[]) external; + function _.upgradeToAndCall(address,bytes) external => NONDET; + function _.ownerOf(uint256 tokenId) external => DISPATCHER(true); + + // Auction manager summaries: + function _.etherfiNodeAddress(uint256) external => NONDET; + function _.updateEtherFiNode(uint256) external => NONDET; + function _.allocateEtherFiNode(bool) external => NONDET; + function _.registerValidator(uint256, bool, address) external => NONDET; + + function auctionManager.numberOfActiveBids() external returns (uint256) envfree; + function auctionManager.isBidActive(uint256) external returns (bool) envfree; +} +// struct DepositData { +// bytes publicKey; +// bytes signature; +// bytes32 depositDataRoot; +// string ipfsHashForEncryptedValidatorKey; +// } + +// struct StakerInfo { +// address staker; +// bytes1 dummy; +// bytes10 hash; +// } + +rule integrityOfBatchDepositWithBidIds(uint256 bidID) { + env e; + uint256[] candidateBidIds = [bidID]; + uint256 numOfValidators; + address validatorSpawner; + address tnftHolder; + address bnftHolder; + bool enableRestaking; + uint256 validatorIds; + + address stakerBefore; + address stakerAfter; + + // get bid information: + bool isActive = auctionManager.isBidActive(bidID); + stakerBefore, _, _ = bidIdToStakerInfo(bidID); + + batchDepositWithBidIds(e, candidateBidIds, numOfValidators, validatorSpawner, tnftHolder, bnftHolder, enableRestaking, validatorIds); + + stakerAfter, _, _ = bidIdToStakerInfo(bidID); + + assert (stakerBefore == 0 && isActive && numOfValidators > 0) => stakerAfter == validatorSpawner; +} + +rule integrityOfBatchCancelDeposit(uint256 validatorId, address caller) { + env e; + uint256[] validatorIds = [validatorId]; + + address stakerBefore; + address stakerAfter; + + stakerBefore, _, _ = bidIdToStakerInfo(validatorId); + + batchCancelDeposit(e, validatorIds, caller); + + stakerAfter, _, _ = bidIdToStakerInfo(validatorId); + + assert stakerBefore == caller && stakerAfter == 0; } -/// @title Verifies that all functions can be called -rule sanity(method f) { +rule integrityOfBatchRegisterValidators(uint256 validatorId) { env e; - calldataarg args; - f(e, args); + uint256 val = e.msg.value; + uint256[] validatorIds = [validatorId]; + address bNftRecipient; + address tNftRecipient; + IStakingManager.DepositData[] depositData; + address validatorSpawner; + + batchRegisterValidators(e, validatorIds, bNftRecipient, tNftRecipient, depositData, validatorSpawner); + satisfy true; -} \ No newline at end of file +} + +rule integrityOfBatchApproveRegistration(uint256 validatorId) { + env e; + uint256 val = e.msg.value; + uint256[] validatorIds = [validatorId]; + bytes[] pubKey; + bytes[] signature; + bytes32[] depositDataRootApproval; + + batchApproveRegistration(e, validatorIds, pubKey, signature, depositDataRootApproval); + + satisfy true; +} diff --git a/certora/specs/TNFT.spec b/certora/specs/TNFT.spec new file mode 100644 index 00000000..2aba50a1 --- /dev/null +++ b/certora/specs/TNFT.spec @@ -0,0 +1,20 @@ +methods { + // IERC721Upgradeable: + function balanceOf(address) external returns (uint256) envfree; + function ownerOf(uint256) external returns (address) envfree; + function safeTransferFrom(address, address, uint256, bytes) external; + function safeTransferFrom(address, address, uint256) external; + function transferFrom(address, address, uint256) external; + function approve(address, uint256) external; + function setApprovalForAll(address, bool) external; + function getApproved(uint256 tokenId) external view returns (address operator); + function isApprovedForAll(address, address) external returns (bool) envfree; + + // TNFT: + function burnFromWithdrawal(uint256) external; + function initialize() external; + function initializeOnUpgrade(address) external; + function mint(address, uint256) external; + function burnFromCancelBNftFlow(uint256) external; + function upgradeTo(address) external; +} From 45a5491d3ca3847164b895504489c1b2cdf3510f Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Sun, 11 Aug 2024 17:05:20 +0300 Subject: [PATCH 08/26] update rules --- certora/config/StakingManager.conf | 8 + certora/specs/EtherFiNodesManager.spec | 65 ++++++++ certora/specs/StakingManager.spec | 208 ++++++++++++++++++++++++- certora/specs/TNFT.spec | 21 +++ certora/specs/nftDispach.spec | 66 ++++++++ 5 files changed, 361 insertions(+), 7 deletions(-) create mode 100644 certora/specs/EtherFiNodesManager.spec create mode 100644 certora/specs/nftDispach.spec diff --git a/certora/config/StakingManager.conf b/certora/config/StakingManager.conf index 790a1d92..76987949 100644 --- a/certora/config/StakingManager.conf +++ b/certora/config/StakingManager.conf @@ -5,10 +5,14 @@ "src/NodeOperatorManager.sol", "src/TNFT.sol", "src/BNFT.sol", + "src/RoleRegistry.sol", + "test/DepositContract.sol" ], "link": [ "StakingManager:auctionManager=AuctionManager", "AuctionManager:nodeOperatorManager=NodeOperatorManager", + "StakingManager:roleRegistry=RoleRegistry", + "StakingManager:depositContractEth2=DepositContract", ], "packages": [ "@openzeppelin=lib/openzeppelin-contracts", @@ -17,7 +21,11 @@ "verify": "StakingManager:certora/specs/StakingManager.spec", "optimistic_loop": true, "optimistic_fallback": true, + "optimistic_hashing": true, + // "parametric_contracts":["StakingManager"], + "build_cache": true, "loop_iter": "3", "solc": "solc8.24", "msg": "all StakingManager", + "rule": ["whoLeaveEth"], } diff --git a/certora/specs/EtherFiNodesManager.spec b/certora/specs/EtherFiNodesManager.spec new file mode 100644 index 00000000..15b5dcab --- /dev/null +++ b/certora/specs/EtherFiNodesManager.spec @@ -0,0 +1,65 @@ +methods { + function _.setValidatorPhase(uint256 _validatorId, uint8 _phase) external => ghostSetValidatorPhase(_validatorId, _phase) expect void; + function _.phase(uint256 _validatorId) external => ghostGetValidatorPhase(_validatorId) expect uint8; +} + +persistent ghost mapping(uint256 => uint8) validatorPhase { + init_state axiom forall uint256 validatorId . validatorPhase[validatorId] == 0; +} + +function ghostSetValidatorPhase(uint256 validatorId, uint8 phase) { + validatorPhase[validatorId] = phase; +} + +function ghostGetValidatorPhase(uint256 validatorId) returns uint8 { + return validatorPhase[validatorId]; +} + +// enum VALIDATOR_PHASE { +// NOT_INITIALIZED,0 +// STAKE_DEPOSITED,1 +// LIVE,2 +// EXITED,3 +// FULLY_WITHDRAWN,4 +// DEPRECATED_CANCELLED,5 +// BEING_SLASHED,6 +// DEPRECATED_EVICTED,7 +// WAITING_FOR_APPROVAL,8 +// DEPRECATED_READY_FOR_DEPOSIT,9 +// } + +// Verify state diafram from documentation. +// State Transition Diagram for StateMachine contract: +// +// NOT_INITIALIZED <- +// | | +// ↓ | +// STAKE_DEPOSITED -- +// / \ | +// ↓ ↓ | +// LIVE <- WAITING_FOR_APPROVAL +// | \ +// | ↓ +// | BEING_SLASHED +// | / +// ↓ ↓ +// EXITED +// | +// ↓ +// FULLY_WITHDRAWN +rule validatorStateTransitions(method f, uint256 validatorId) { + env e; + calldataarg args; + + uint8 phaseBefore = validatorPhase[validatorId]; + f(e, args); + uint8 phaseAfter = validatorPhase[validatorId]; + + assert phaseAfter == 0 => phaseBefore == 0 || phaseBefore == 1 || phaseBefore == 8, "NOT_INITIALIZED transtion violated"; + assert phaseAfter == 1 => phaseBefore == 0, "STAKE_DEPOSITED transtion violated"; + assert phaseAfter == 2 => phaseBefore == 1 || phaseBefore == 8, "LIVE transtion violated"; + assert phaseAfter == 3 => phaseBefore == 2 || phaseBefore == 6, "EXITED transtion violated"; + assert phaseAfter == 4 => phaseBefore == 3, "FULLY_WITHDRAWN transtion violated"; + assert phaseAfter == 6 => phaseBefore == 2, "BEING_SLASHED transtion violated"; + assert phaseAfter == 8 => phaseBefore == 1, "WAITING_FOR_APPROVAL transtion violated"; +} diff --git a/certora/specs/StakingManager.spec b/certora/specs/StakingManager.spec index 01ada430..c8f86893 100644 --- a/certora/specs/StakingManager.spec +++ b/certora/specs/StakingManager.spec @@ -1,10 +1,15 @@ +import "./nftDispach.spec"; +import "./EtherFiNodesManager.spec"; + using AuctionManager as auctionManager; + methods { // Getters: function maxBatchDepositSize() external returns (uint128) envfree; function stakeAmount() external returns (uint128) envfree; function liquidityPoolContract() external returns (address) envfree; function bidIdToStakerInfo(uint256) external returns (address, bytes1, bytes10) envfree; + function depositContractEth2() external returns (address) envfree; function initialize(address, address) external; function initializeOnUpgrade(address, address) external; @@ -14,17 +19,34 @@ methods { function batchApproveRegistration(uint256[], bytes[], bytes[], bytes32[]) external; function _.upgradeToAndCall(address,bytes) external => NONDET; - function _.ownerOf(uint256 tokenId) external => DISPATCHER(true); - // Auction manager summaries: + // Node manager summaries: function _.etherfiNodeAddress(uint256) external => NONDET; function _.updateEtherFiNode(uint256) external => NONDET; function _.allocateEtherFiNode(bool) external => NONDET; function _.registerValidator(uint256, bool, address) external => NONDET; + function _.unregisterValidator(uint256) external => CONSTANT; + function _.getWithdrawalCredentials(uint256) external => NONDET; + function _.incrementNumberOfValidators(uint256) external => NONDET; + + function _.generateDepositRoot(bytes, bytes, bytes, uint256) external => NONDET; + + // roleRegistry summaries: + // function _.hasRole(address) external => NONDET; + // function hasRole(bytes32, address) external => NONDET; function auctionManager.numberOfActiveBids() external returns (uint256) envfree; function auctionManager.isBidActive(uint256) external returns (bool) envfree; + function auctionManager.membershipManagerContractAddress() external returns (address) envfree; } + +// Functions filtered out since they use `delegatecall`. +definition isFilteredFunc(method f) returns bool = ( + f.selector == sig:upgradeToAndCall(address, bytes).selector +); + +definition wei() returns uint256 = 1000000000000000000; + // struct DepositData { // bytes publicKey; // bytes signature; @@ -37,6 +59,18 @@ methods { // bytes1 dummy; // bytes10 hash; // } +rule whoLeaveEth(method f, address membershipAddress) + filtered { f -> !isFilteredFunc(f) } { + env e; + require membershipAddress != e.msg.sender; + require auctionManager.membershipManagerContractAddress() == membershipAddress; + calldataarg args; + uint256 contractBalancePre = nativeBalances[currentContract]; + f(e,args); + uint256 contractBalancePost = nativeBalances[currentContract]; + assert contractBalancePre == contractBalancePost; +} + rule integrityOfBatchDepositWithBidIds(uint256 bidID) { env e; @@ -52,44 +86,195 @@ rule integrityOfBatchDepositWithBidIds(uint256 bidID) { address stakerAfter; // get bid information: - bool isActive = auctionManager.isBidActive(bidID); + bool isActiveBefore = auctionManager.isBidActive(bidID); stakerBefore, _, _ = bidIdToStakerInfo(bidID); batchDepositWithBidIds(e, candidateBidIds, numOfValidators, validatorSpawner, tnftHolder, bnftHolder, enableRestaking, validatorIds); + bool isActiveAfter = auctionManager.isBidActive(bidID); stakerAfter, _, _ = bidIdToStakerInfo(bidID); - assert (stakerBefore == 0 && isActive && numOfValidators > 0) => stakerAfter == validatorSpawner; + assert (stakerBefore == 0 && isActiveBefore && numOfValidators > 0) => stakerAfter == validatorSpawner && !isActiveAfter; } rule integrityOfBatchCancelDeposit(uint256 validatorId, address caller) { env e; + require e.msg.sender != currentContract; + require e.msg.sender != auctionManager; uint256[] validatorIds = [validatorId]; address stakerBefore; address stakerAfter; + mathint ethBalanceBefore = nativeBalances[e.msg.sender]; stakerBefore, _, _ = bidIdToStakerInfo(validatorId); batchCancelDeposit(e, validatorIds, caller); stakerAfter, _, _ = bidIdToStakerInfo(validatorId); + mathint ethBalanceAfter = nativeBalances[e.msg.sender]; + bool isActiveAfter = auctionManager.isBidActive(validatorId); + + assert stakerBefore == caller && stakerAfter == 0, "wrong staker settings"; + assert ethBalanceAfter == ethBalanceBefore + 32, "stake didn't fully refunded"; + assert isActiveAfter, "The bid didn't reenter the auction"; +} + +// tokens are burned: +// TNFTInterfaceInstance.burnFromCancelBNftFlow(nftTokenId); +// BNFTInterfaceInstance.burnFromCancelBNftFlow(nftTokenId); +// no token owner +// owner nftBalance decresed by 1 for each token burned + +rule batchCancelDepositFR(method f, uint256 validatorId, address caller) + filtered { f -> !isFilteredFunc(f) + && f.selector != sig:pauseContract().selector + || f.selector != sig:instantiateEtherFiNode(bool).selector + || f.selector != sig:initialize(address,address).selector } { + env e; + env eFr; + calldataarg args; + require eFr.msg.sender != e.msg.sender; + require e.msg.sender != currentContract; + require e.msg.sender != auctionManager; + require eFr.msg.sender != currentContract; + require eFr.msg.sender != auctionManager; + require e.msg.sender != 0; + require eFr.msg.sender != 0; + uint256[] validatorIds = [validatorId]; + + storage initState = lastStorage; + + batchCancelDeposit(e, validatorIds, caller); + + f(eFr, args) at initState; + + batchCancelDeposit@withrevert(e, validatorIds, caller); + + bool didRvert = lastReverted; + + assert !didRvert; +} + +rule batchDepositFR(method f, uint256 bidID) + filtered { f -> !isFilteredFunc(f) + && f.selector != sig:pauseContract().selector + || f.selector != sig:instantiateEtherFiNode(bool).selector + || f.selector != sig:initialize(address,address).selector } { + env e; + env eFr; + calldataarg args; + require eFr.msg.sender != e.msg.sender; + require e.msg.sender != currentContract; + require e.msg.sender != auctionManager; + require eFr.msg.sender != currentContract; + require eFr.msg.sender != auctionManager; + require e.msg.sender != 0; + require eFr.msg.sender != 0; + uint256[] candidateBidIds = [bidID]; + uint256 numOfValidators; + address validatorSpawner; + address tnftHolder; + address bnftHolder; + bool enableRestaking; + uint256 validatorIds; - assert stakerBefore == caller && stakerAfter == 0; + storage initState = lastStorage; + + batchDepositWithBidIds(e, candidateBidIds, numOfValidators, validatorSpawner, tnftHolder, bnftHolder, enableRestaking, validatorIds); + + f(eFr, args) at initState; + + batchDepositWithBidIds@withrevert(e, candidateBidIds, numOfValidators, validatorSpawner, tnftHolder, bnftHolder, enableRestaking, validatorIds); + + bool didRvert = lastReverted; + + assert !didRvert; +} + +rule batchRegisterValidatorsFR(method f, uint256 bidID) + filtered { f -> !isFilteredFunc(f) + && f.selector != sig:pauseContract().selector + || f.selector != sig:instantiateEtherFiNode(bool).selector + || f.selector != sig:initialize(address,address).selector } { + env e; + env eFr; + calldataarg specificArgs; + calldataarg args; + require eFr.msg.sender != e.msg.sender; + require e.msg.sender != currentContract; + require e.msg.sender != auctionManager; + require eFr.msg.sender != currentContract; + require eFr.msg.sender != auctionManager; + require e.msg.sender != 0; + require eFr.msg.sender != 0; + + storage initState = lastStorage; + + batchRegisterValidators(e, specificArgs); + + f(eFr, args) at initState; + + batchRegisterValidators@withrevert(e, specificArgs); + + bool didRvert = lastReverted; + + assert !didRvert; +} + +rule batchApproveRegistrationFR(method f, uint256 bidID) + filtered { f -> !isFilteredFunc(f) + && f.selector != sig:pauseContract().selector + || f.selector != sig:instantiateEtherFiNode(bool).selector + || f.selector != sig:initialize(address,address).selector } { + env e; + env eFr; + calldataarg args; + calldataarg specificArgs; + require eFr.msg.sender != e.msg.sender; + require e.msg.sender != currentContract; + require e.msg.sender != auctionManager; + require eFr.msg.sender != currentContract; + require eFr.msg.sender != auctionManager; + require e.msg.sender != 0; + require eFr.msg.sender != 0; + + storage initState = lastStorage; + + batchApproveRegistration(e, specificArgs); + + f(eFr, args) at initState; + + batchApproveRegistration@withrevert(e, specificArgs); + + bool didRvert = lastReverted; + + assert !didRvert; } rule integrityOfBatchRegisterValidators(uint256 validatorId) { env e; - uint256 val = e.msg.value; + uint256 value = e.msg.value; // == wei() * validatorIds.length uint256[] validatorIds = [validatorId]; address bNftRecipient; address tNftRecipient; IStakingManager.DepositData[] depositData; address validatorSpawner; + // LiquidityPool requirements: + require depositData.length == validatorIds.length; + + uint256 contractBalancePre = nativeBalances[currentContract]; + batchRegisterValidators(e, validatorIds, bNftRecipient, tNftRecipient, depositData, validatorSpawner); - satisfy true; + uint8 _validatorPhase = validatorPhase[validatorId]; + uint256 contractBalancePost = nativeBalances[currentContract]; + + // assert validator phase: + assert _validatorPhase == 2 || _validatorPhase == 8; + // processAuctionFeeTransfer + // NFTS are correctly minted. } rule integrityOfBatchApproveRegistration(uint256 validatorId) { @@ -100,7 +285,16 @@ rule integrityOfBatchApproveRegistration(uint256 validatorId) { bytes[] signature; bytes32[] depositDataRootApproval; + // LiquidityPool requirements: + require validatorIds.length == pubKey.length; + require validatorIds.length == signature.length; + batchApproveRegistration(e, validatorIds, pubKey, signature, depositDataRootApproval); + uint8 _validatorPhase = validatorPhase[validatorId]; + + // assert validator phase: satisfy true; } + + diff --git a/certora/specs/TNFT.spec b/certora/specs/TNFT.spec index 2aba50a1..14c0e90c 100644 --- a/certora/specs/TNFT.spec +++ b/certora/specs/TNFT.spec @@ -18,3 +18,24 @@ methods { function burnFromCancelBNftFlow(uint256) external; function upgradeTo(address) external; } + +ghost mapping(uint256 => address) owners { + init_state axiom forall uint256 id . owners[id] == 0; +} + +ghost mathint sumAllTNFT { + init_state axiom sumAllTNFT == 0; +} + +hook Sstore _owners[KEY uint256 id] address newOwner (address oldOwner) { + if(oldOwner == 0 && newOwner != 0) { + sumAllTNFT = sumAllTNFT + 1; + } else if(newOwner == 0 && oldOwner != 0) { + sumAllTNFT = sumAllTNFT 1 1; + } + owners[id] = newOwner; +} + +hook Sload address owner _owners[KEY uint256 id] { + require owner == owners[id]; +} diff --git a/certora/specs/nftDispach.spec b/certora/specs/nftDispach.spec new file mode 100644 index 00000000..762773d9 --- /dev/null +++ b/certora/specs/nftDispach.spec @@ -0,0 +1,66 @@ +using TNFT as tnft; +using BNFT as bnft; + +methods { + // IERC721Upgradeable: + function _.balanceOf(address) external => DISPATCHER(true); + function _.ownerOf(uint256) external => DISPATCHER(true); + function _.safeTransferFrom(address, address, uint256, bytes) external => DISPATCHER(true); + function _.safeTransferFrom(address, address, uint256) external => DISPATCHER(true); + function _.transferFrom(address, address, uint256) external => DISPATCHER(true); + function _.approve(address, uint256) external => DISPATCHER(true); + function _.setApprovalForAll(address, bool) external => DISPATCHER(true); + function _.getApproved(uint256) external => DISPATCHER(true); + function _.isApprovedForAll(address, address) external => DISPATCHER(true); + + // BNFT: + function _.burnFromWithdrawal(uint256) external => DISPATCHER(true); + function _.initialize() external => DISPATCHER(true); + function _.initializeOnUpgrade(address) external => DISPATCHER(true); + function _.mint(address, uint256) external => DISPATCHER(true); + function _.burnFromCancelBNftFlow(uint256) external => DISPATCHER(true); + function _.upgradeTo(address) external => DISPATCHER(true); +} + +persistent ghost mapping(uint256 => address) tnftOwners { + init_state axiom forall uint256 id . tnftOwners[id] == 0; +} + +persistent ghost mathint sumAllTNFT { + init_state axiom sumAllTNFT == 0; +} + +persistent ghost mapping(uint256 => address) bnftOwners { + init_state axiom forall uint256 id . bnftOwners[id] == 0; +} + +persistent ghost mathint sumAllBNFT { + init_state axiom sumAllBNFT == 0; +} + +hook Sstore tnft._owners[KEY uint256 id] address newOwner (address oldOwner) { + if(oldOwner == 0 && newOwner != 0) { + sumAllTNFT = sumAllTNFT + 1; + } else if(newOwner == 0 && oldOwner != 0) { + sumAllTNFT = sumAllTNFT - 1; + } + tnftOwners[id] = newOwner; +} + +hook Sload address owner tnft._owners[KEY uint256 id] { + require owner == tnftOwners[id]; +} + +hook Sstore bnft._owners[KEY uint256 id] address newOwner (address oldOwner) { + if(oldOwner == 0 && newOwner != 0) { + sumAllBNFT = sumAllBNFT + 1; + } else if(newOwner == 0 && oldOwner != 0) { + sumAllBNFT = sumAllBNFT - 1; + } + bnftOwners[id] = newOwner; +} + +hook Sload address owner bnft._owners[KEY uint256 id] { + require owner == bnftOwners[id]; +} + From 9cb729be971bd306353cc3cd610ea782e2adb229 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Sun, 11 Aug 2024 17:25:46 +0300 Subject: [PATCH 09/26] align spec with new code --- certora/specs/StakingManager.spec | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/certora/specs/StakingManager.spec b/certora/specs/StakingManager.spec index c8f86893..62631dae 100644 --- a/certora/specs/StakingManager.spec +++ b/certora/specs/StakingManager.spec @@ -13,9 +13,9 @@ methods { function initialize(address, address) external; function initializeOnUpgrade(address, address) external; - function batchDepositWithBidIds(uint256[], uint256, address, address, address, bool, uint256) external returns (uint256[] memory); + function batchDepositWithBidIds(uint256[], uint256, address, address, bool, uint256) external returns (uint256[] memory); function batchCancelDeposit(uint256[], address) external; - function batchRegisterValidators(uint256[], address, address, IStakingManager.DepositData[], address) external; + function batchRegisterValidators(uint256[], address, address, IStakingManager.DepositData[]) external; function batchApproveRegistration(uint256[], bytes[], bytes[], bytes32[]) external; function _.upgradeToAndCall(address,bytes) external => NONDET; @@ -76,7 +76,6 @@ rule integrityOfBatchDepositWithBidIds(uint256 bidID) { env e; uint256[] candidateBidIds = [bidID]; uint256 numOfValidators; - address validatorSpawner; address tnftHolder; address bnftHolder; bool enableRestaking; @@ -89,12 +88,12 @@ rule integrityOfBatchDepositWithBidIds(uint256 bidID) { bool isActiveBefore = auctionManager.isBidActive(bidID); stakerBefore, _, _ = bidIdToStakerInfo(bidID); - batchDepositWithBidIds(e, candidateBidIds, numOfValidators, validatorSpawner, tnftHolder, bnftHolder, enableRestaking, validatorIds); + batchDepositWithBidIds(e, candidateBidIds, numOfValidators, tnftHolder, bnftHolder, enableRestaking, validatorIds); bool isActiveAfter = auctionManager.isBidActive(bidID); stakerAfter, _, _ = bidIdToStakerInfo(bidID); - assert (stakerBefore == 0 && isActiveBefore && numOfValidators > 0) => stakerAfter == validatorSpawner && !isActiveAfter; + assert (stakerBefore == 0 && isActiveBefore && numOfValidators > 0) => stakerAfter == bnftHolder && !isActiveAfter; } rule integrityOfBatchCancelDeposit(uint256 validatorId, address caller) { @@ -173,7 +172,6 @@ rule batchDepositFR(method f, uint256 bidID) require eFr.msg.sender != 0; uint256[] candidateBidIds = [bidID]; uint256 numOfValidators; - address validatorSpawner; address tnftHolder; address bnftHolder; bool enableRestaking; @@ -181,11 +179,11 @@ rule batchDepositFR(method f, uint256 bidID) storage initState = lastStorage; - batchDepositWithBidIds(e, candidateBidIds, numOfValidators, validatorSpawner, tnftHolder, bnftHolder, enableRestaking, validatorIds); + batchDepositWithBidIds(e, candidateBidIds, numOfValidators, tnftHolder, bnftHolder, enableRestaking, validatorIds); f(eFr, args) at initState; - batchDepositWithBidIds@withrevert(e, candidateBidIds, numOfValidators, validatorSpawner, tnftHolder, bnftHolder, enableRestaking, validatorIds); + batchDepositWithBidIds@withrevert(e, candidateBidIds, numOfValidators, tnftHolder, bnftHolder, enableRestaking, validatorIds); bool didRvert = lastReverted; @@ -259,14 +257,13 @@ rule integrityOfBatchRegisterValidators(uint256 validatorId) { address bNftRecipient; address tNftRecipient; IStakingManager.DepositData[] depositData; - address validatorSpawner; // LiquidityPool requirements: require depositData.length == validatorIds.length; uint256 contractBalancePre = nativeBalances[currentContract]; - batchRegisterValidators(e, validatorIds, bNftRecipient, tNftRecipient, depositData, validatorSpawner); + batchRegisterValidators(e, validatorIds, bNftRecipient, tNftRecipient, depositData); uint8 _validatorPhase = validatorPhase[validatorId]; uint256 contractBalancePost = nativeBalances[currentContract]; From c0fece60c916e2ef2b73277c8c7cc0c942f84e45 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Mon, 12 Aug 2024 14:31:48 +0300 Subject: [PATCH 10/26] update nfts rules --- certora/specs/StakingManager.spec | 50 +++++++++++-------------------- certora/specs/nftDispach.spec | 41 +++++++++++++++++++++++++ 2 files changed, 59 insertions(+), 32 deletions(-) diff --git a/certora/specs/StakingManager.spec b/certora/specs/StakingManager.spec index 62631dae..908b9053 100644 --- a/certora/specs/StakingManager.spec +++ b/certora/specs/StakingManager.spec @@ -47,18 +47,7 @@ definition isFilteredFunc(method f) returns bool = ( definition wei() returns uint256 = 1000000000000000000; -// struct DepositData { -// bytes publicKey; -// bytes signature; -// bytes32 depositDataRoot; -// string ipfsHashForEncryptedValidatorKey; -// } - -// struct StakerInfo { -// address staker; -// bytes1 dummy; -// bytes10 hash; -// } +// rule for research purpose. rule whoLeaveEth(method f, address membershipAddress) filtered { f -> !isFilteredFunc(f) } { env e; @@ -107,24 +96,26 @@ rule integrityOfBatchCancelDeposit(uint256 validatorId, address caller) { mathint ethBalanceBefore = nativeBalances[e.msg.sender]; stakerBefore, _, _ = bidIdToStakerInfo(validatorId); + uint8 phasePre = validatorPhase[validatorId]; + mathint tnftAmountPre = sumAllTNFT; + mathint bnftAmountPre = sumAllBNFT; batchCancelDeposit(e, validatorIds, caller); stakerAfter, _, _ = bidIdToStakerInfo(validatorId); mathint ethBalanceAfter = nativeBalances[e.msg.sender]; bool isActiveAfter = auctionManager.isBidActive(validatorId); + mathint tnftAmountPost = sumAllTNFT; + mathint bnftAmountPost = sumAllBNFT; assert stakerBefore == caller && stakerAfter == 0, "wrong staker settings"; - assert ethBalanceAfter == ethBalanceBefore + 32, "stake didn't fully refunded"; + assert liquidityPoolContract() != e.msg.sender => ethBalanceAfter == ethBalanceBefore + 32, "stake didn't fully refunded"; assert isActiveAfter, "The bid didn't reenter the auction"; + assert phasePre == 8 => (tnftAmountPost == tnftAmountPre - 1) && + (bnftAmountPost == bnftAmountPre - 1), "nfts wasn't burned when pre validator phase was WAITING_FOR_APPROVAL"; + assert phasePre == 8 => bnft.ownerOf(e, validatorId) == 0 && tnft.ownerOf(e, validatorId) == 0, "wrong nfts were burned"; } -// tokens are burned: -// TNFTInterfaceInstance.burnFromCancelBNftFlow(nftTokenId); -// BNFTInterfaceInstance.burnFromCancelBNftFlow(nftTokenId); -// no token owner -// owner nftBalance decresed by 1 for each token burned - rule batchCancelDepositFR(method f, uint256 validatorId, address caller) filtered { f -> !isFilteredFunc(f) && f.selector != sig:pauseContract().selector @@ -137,7 +128,7 @@ rule batchCancelDepositFR(method f, uint256 validatorId, address caller) require e.msg.sender != currentContract; require e.msg.sender != auctionManager; require eFr.msg.sender != currentContract; - require eFr.msg.sender != auctionManager; + // require eFr.msg.sender != auctionManager; require e.msg.sender != 0; require eFr.msg.sender != 0; uint256[] validatorIds = [validatorId]; @@ -155,7 +146,7 @@ rule batchCancelDepositFR(method f, uint256 validatorId, address caller) assert !didRvert; } -rule batchDepositFR(method f, uint256 bidID) +rule batchDepositFR(method f) filtered { f -> !isFilteredFunc(f) && f.selector != sig:pauseContract().selector || f.selector != sig:instantiateEtherFiNode(bool).selector @@ -167,23 +158,18 @@ rule batchDepositFR(method f, uint256 bidID) require e.msg.sender != currentContract; require e.msg.sender != auctionManager; require eFr.msg.sender != currentContract; - require eFr.msg.sender != auctionManager; + // require eFr.msg.sender != auctionManager; require e.msg.sender != 0; require eFr.msg.sender != 0; - uint256[] candidateBidIds = [bidID]; - uint256 numOfValidators; - address tnftHolder; - address bnftHolder; - bool enableRestaking; - uint256 validatorIds; + calldataarg specificArgs; storage initState = lastStorage; - batchDepositWithBidIds(e, candidateBidIds, numOfValidators, tnftHolder, bnftHolder, enableRestaking, validatorIds); + batchDepositWithBidIds(e, specificArgs); f(eFr, args) at initState; - batchDepositWithBidIds@withrevert(e, candidateBidIds, numOfValidators, tnftHolder, bnftHolder, enableRestaking, validatorIds); + batchDepositWithBidIds@withrevert(e, specificArgs); bool didRvert = lastReverted; @@ -203,7 +189,7 @@ rule batchRegisterValidatorsFR(method f, uint256 bidID) require e.msg.sender != currentContract; require e.msg.sender != auctionManager; require eFr.msg.sender != currentContract; - require eFr.msg.sender != auctionManager; + // require eFr.msg.sender != auctionManager; require e.msg.sender != 0; require eFr.msg.sender != 0; @@ -233,7 +219,7 @@ rule batchApproveRegistrationFR(method f, uint256 bidID) require e.msg.sender != currentContract; require e.msg.sender != auctionManager; require eFr.msg.sender != currentContract; - require eFr.msg.sender != auctionManager; + // require eFr.msg.sender != auctionManager; require e.msg.sender != 0; require eFr.msg.sender != 0; diff --git a/certora/specs/nftDispach.spec b/certora/specs/nftDispach.spec index 762773d9..d8837116 100644 --- a/certora/specs/nftDispach.spec +++ b/certora/specs/nftDispach.spec @@ -26,18 +26,34 @@ persistent ghost mapping(uint256 => address) tnftOwners { init_state axiom forall uint256 id . tnftOwners[id] == 0; } +persistent ghost mapping(address => uint256) tntBalances { + init_state axiom forall address owner . tntBalances[owner] == 0; +} + persistent ghost mathint sumAllTNFT { init_state axiom sumAllTNFT == 0; } +persistent ghost mathint sumAllTNFTBalances { + init_state axiom sumAllTNFTBalances == 0; +} + persistent ghost mapping(uint256 => address) bnftOwners { init_state axiom forall uint256 id . bnftOwners[id] == 0; } +persistent ghost mapping(address => uint256) bntBalances { + init_state axiom forall address owner . bntBalances[owner] == 0; +} + persistent ghost mathint sumAllBNFT { init_state axiom sumAllBNFT == 0; } +persistent ghost mathint sumAllBNFTBalances { + init_state axiom sumAllBNFTBalances == 0; +} + hook Sstore tnft._owners[KEY uint256 id] address newOwner (address oldOwner) { if(oldOwner == 0 && newOwner != 0) { sumAllTNFT = sumAllTNFT + 1; @@ -64,3 +80,28 @@ hook Sload address owner bnft._owners[KEY uint256 id] { require owner == bnftOwners[id]; } +hook Sstore tnft._balances[KEY address owner] uint256 newCount (uint256 oldCount) { + sumAllTNFTBalances = sumAllTNFTBalances - oldCount + newCount; + tntBalances[owner] = newCount; +} + +hook Sload uint256 count tnft._balances[KEY address owner] { + require count == tntBalances[owner]; +} + +hook Sstore bnft._balances[KEY address owner] uint256 newCount (uint256 oldCount) { + sumAllBNFTBalances = sumAllBNFTBalances - oldCount + newCount; + bntBalances[owner] = newCount; +} + +hook Sload uint256 count bnft._balances[KEY address owner] { + require count == bntBalances[owner]; +} + +// amount of tnfts with owner equals the sum of every tnft owner balance. +invariant sumAllTNFTEqSumAllTNFTBalances() + sumAllTNFTBalances == sumAllTNFT; + +// amount of bnfts with owner equals the sum of every bnft owner balance. +invariant sumAllBNFTEqSumAllBNFTBalances() + sumAllBNFTBalances == sumAllBNFT; From 2fab56ec05b7ef851b6ab6a501105582e2581379 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Mon, 26 Aug 2024 17:00:38 +0300 Subject: [PATCH 11/26] update auction manager spec --- certora/specs/AuctionManager.spec | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/certora/specs/AuctionManager.spec b/certora/specs/AuctionManager.spec index 0ace7ea9..cabdc0ae 100644 --- a/certora/specs/AuctionManager.spec +++ b/certora/specs/AuctionManager.spec @@ -14,6 +14,8 @@ methods { function bids(uint256) external returns (uint256, uint64, address, bool) envfree; function getBidOwner(uint256) external returns (address) envfree; function isBidActive(uint256) external returns (bool) envfree; + function accumulatedRevenue() external returns (uint128) envfree; + function accumulatedRevenueThreshold() external returns (uint128) envfree; function NodeOperatorManager.getUserTotalKeys(address) external returns (uint64) envfree; function NodeOperatorManager.getNumKeysRemaining(address) external returns (uint64) envfree; @@ -32,17 +34,26 @@ invariant numberOfActiveBidsCorrect() // numberOfBids equals the sum of all bids. invariant numberOfBidsEqTheSumOfAllBids() sum_of_bids == to_mathint(numberOfBids()) - filtered {f -> !isFilteredFunc(f)} + filtered {f -> !isFilteredFunc(f) && f.selector != sig:initialize(address).selector} // solvency invariant - contract should hold atleast sumOfAllActiveBidAmounts amount of eth. invariant activeBidsSolvency() to_mathint(nativeBalances[currentContract]) >= sum_of_all_active_bids_amounts filtered {f -> !isFilteredFunc(f)} + { + preserved with (env e) { + require e.msg.sender != currentContract; + } + preserved processAuctionFeeTransfer(uint256 bidId) with (env e) { + // bidId must be inactive (because there is a stacker that is not address zero). + require isBidActive(bidId) == false; + } + } // the sum of all used keys equals num of bids. // invariant numOfAllUsedKeysEqNumOfBids() {} -// chack for all bids to see if the key index is unique per user. +// chack for all bids to see if the key index is unique per user. / not same user with same keyIndex on different bids: // rule bidderPubKeyIndexIsUniqePerUser() {} rule bidImmutability(method f, uint256 bid_id) filtered {f -> !isFilteredFunc(f)} { @@ -117,13 +128,3 @@ rule integrityOfCreateBid(uint256 _bidSize, uint256 _bidAmountPerBid) { // rule integrityOfCancelBid(uint256 bidId) { // env e; // } - -// rule onlyWhiteListCanBid() {} - -/// @title Verifies that all functions can be called -rule sanity(method f) { - env e; - calldataarg args; - f(e, args); - satisfy true; -} \ No newline at end of file From 20749f2abd3349d46c9157f58efd0f82601de209 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Mon, 26 Aug 2024 21:13:06 +0300 Subject: [PATCH 12/26] update staking manager spec --- certora/specs/StakingManager.spec | 26 ++++++++++++++++---------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/certora/specs/StakingManager.spec b/certora/specs/StakingManager.spec index 908b9053..80e96416 100644 --- a/certora/specs/StakingManager.spec +++ b/certora/specs/StakingManager.spec @@ -27,19 +27,18 @@ methods { function _.registerValidator(uint256, bool, address) external => NONDET; function _.unregisterValidator(uint256) external => CONSTANT; function _.getWithdrawalCredentials(uint256) external => NONDET; - function _.incrementNumberOfValidators(uint256) external => NONDET; - + function _.incrementNumberOfValidators(uint64) external => NONDET; function _.generateDepositRoot(bytes, bytes, bytes, uint256) external => NONDET; - // roleRegistry summaries: - // function _.hasRole(address) external => NONDET; - // function hasRole(bytes32, address) external => NONDET; - function auctionManager.numberOfActiveBids() external returns (uint256) envfree; function auctionManager.isBidActive(uint256) external returns (bool) envfree; function auctionManager.membershipManagerContractAddress() external returns (address) envfree; + function auctionManager.processAuctionFeeTransfer(uint256) external => NONDET; } +use invariant sumAllTNFTEqSumAllTNFTBalances; +use invariant sumAllBNFTEqSumAllBNFTBalances; + // Functions filtered out since they use `delegatecall`. definition isFilteredFunc(method f) returns bool = ( f.selector == sig:upgradeToAndCall(address, bytes).selector @@ -60,7 +59,6 @@ rule whoLeaveEth(method f, address membershipAddress) assert contractBalancePre == contractBalancePost; } - rule integrityOfBatchDepositWithBidIds(uint256 bidID) { env e; uint256[] candidateBidIds = [bidID]; @@ -238,6 +236,7 @@ rule batchApproveRegistrationFR(method f, uint256 bidID) rule integrityOfBatchRegisterValidators(uint256 validatorId) { env e; + require e.msg.sender != currentContract; uint256 value = e.msg.value; // == wei() * validatorIds.length uint256[] validatorIds = [validatorId]; address bNftRecipient; @@ -248,16 +247,25 @@ rule integrityOfBatchRegisterValidators(uint256 validatorId) { require depositData.length == validatorIds.length; uint256 contractBalancePre = nativeBalances[currentContract]; + mathint tnftAmountPre = sumAllTNFT; + mathint bnftAmountPre = sumAllBNFT; batchRegisterValidators(e, validatorIds, bNftRecipient, tNftRecipient, depositData); uint8 _validatorPhase = validatorPhase[validatorId]; uint256 contractBalancePost = nativeBalances[currentContract]; + mathint tnftAmountPost = sumAllTNFT; + mathint bnftAmountPost = sumAllBNFT; // assert validator phase: assert _validatorPhase == 2 || _validatorPhase == 8; - // processAuctionFeeTransfer + // processAuctionFeeTransfer - not needed, covered by auctionManager spec. // NFTS are correctly minted. + assert contractBalancePre == contractBalancePost, "eth was left in the contract"; + assert tnftAmountPost == tnftAmountPre + 1, "tnft wasn't minted"; + assert bnftAmountPost == bnftAmountPre + 1, "bnft wasn't minted"; + assert tnft.ownerOf(e, validatorId) == tNftRecipient, "tnft was minted for the wrong user"; + assert bnft.ownerOf(e, validatorId) == bNftRecipient, "bnft was minted for the wrong user"; } rule integrityOfBatchApproveRegistration(uint256 validatorId) { @@ -279,5 +287,3 @@ rule integrityOfBatchApproveRegistration(uint256 validatorId) { // assert validator phase: satisfy true; } - - From b7255fec355bdc4b1a5a9c5f5517ce6dd540709c Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Tue, 27 Aug 2024 01:51:33 +0300 Subject: [PATCH 13/26] etherfi node specs --- certora/config/EtherFiNode.conf | 21 +++ certora/specs/EtherFiNode.spec | 174 +++++++++++++++++++++++++ certora/specs/EtherFiNodeSetup.spec | 174 +++++++++++++++++++++++++ certora/specs/EtherFiNodesManager.spec | 80 +++++++----- 4 files changed, 416 insertions(+), 33 deletions(-) create mode 100644 certora/config/EtherFiNode.conf create mode 100644 certora/specs/EtherFiNode.spec create mode 100644 certora/specs/EtherFiNodeSetup.spec diff --git a/certora/config/EtherFiNode.conf b/certora/config/EtherFiNode.conf new file mode 100644 index 00000000..74732ad9 --- /dev/null +++ b/certora/config/EtherFiNode.conf @@ -0,0 +1,21 @@ +{ + "files": [ + "src/EtherFiNode.sol", + ], + "link": [ + ], + "packages": [ + "@openzeppelin=lib/openzeppelin-contracts", + "forge-std=lib/forge-std/src" + ], + "verify": "EtherFiNode:certora/specs/EtherFiNode.spec", + "optimistic_loop": true, + "optimistic_fallback": true, + "optimistic_hashing": true, + // "parametric_contracts":["EtherFiNode"], + "build_cache": true, + "loop_iter": "3", + "solc": "solc8.24", + "msg": "EtherFiNode", + "rule": ["registerValidatorThenUnregisteringNeverReverts", "associatedValidatorIdsLengthEqNumOfValidators"], +} diff --git a/certora/specs/EtherFiNode.spec b/certora/specs/EtherFiNode.spec new file mode 100644 index 00000000..489d8654 --- /dev/null +++ b/certora/specs/EtherFiNode.spec @@ -0,0 +1,174 @@ +import "./EtherFiNodeSetup.spec"; + +use invariant mirrorLength; +use invariant validatorPastLengthAreNullified; +use invariant validatorIndeciesLessThanLength; +use invariant validatorIndeciesValidaorIdMirror; +use invariant blockNumberValidity; +use invariant validatorIdsAreUnique; +use invariant validatorIdNeverZero; +use builtin rule sanity; + +rule integrityRegisterValidator(uint256 validatorId, bool enableRestaking) { + env e; + requireInvariant validatorIndeciesValidaorIdMirror(); + require version() == 1; + require validatorId != 0; + + mathint numOfValidatorsPre = sumAllAssociatedValidatorIds; + require numOfValidatorsPre < max_uint256; + + bool validatorExistsPre = (associatedValidatorIndicesGhost[validatorId] != 0); + + registerValidator(e, validatorId, enableRestaking); + + bool validatorExistsPost = (associatedValidatorIndicesGhost[validatorId] != 0); + + mathint numOfValidatorsPost = sumAllAssociatedValidatorIds; + + assert !validatorExistsPre && validatorExistsPost => numOfValidatorsPost == numOfValidatorsPre + 1; + assert !validatorExistsPre => associatedValidatorIdsGhost[assert_uint256(numOfValidatorsPre)] == validatorId; + assert !validatorExistsPre => associatedValidatorIndicesGhost[validatorId] == numOfValidatorsPre; +} + +rule integrityOfUnregisterValidator(uint256 validatorId, IEtherFiNodesManager.ValidatorInfo info) { + env e; + bool succeed; + + mathint numOfValidatorsPre = sumAllAssociatedValidatorIds; + + bool validatorExistsPre = (associatedValidatorIndicesGhost[validatorId] != 0); + + succeed = unRegisterValidator(e, validatorId, info); + + bool validatorExistsPost = (associatedValidatorIndicesGhost[validatorId] != 0); + assert false; +} + +rule pendingComplitedWithdrawalsCorrelation(method f) { + env e; + calldataarg args; + + uint64 pendingPre = pendingWithdrawalFromRestakingInGwei(); + uint64 completedPre = completedWithdrawalFromRestakingInGwei(); + + f(e, args); + + uint64 pendingPost = pendingWithdrawalFromRestakingInGwei(); + uint64 completedPost = completedWithdrawalFromRestakingInGwei(); + + assert pendingPost < pendingPre => completedPost > completedPre; +} + +rule whoLeaveEth(method f, address membershipAddress) { + env e; + // require membershipAddress != e.msg.sender; + // require auctionManager.membershipManagerContractAddress() == membershipAddress; + calldataarg args; + uint256 contractBalancePre = nativeBalances[currentContract]; + f(e,args); + uint256 contractBalancePost = nativeBalances[currentContract]; + assert contractBalancePre == contractBalancePost; +} + +// Verify state diafram from documentation. +// State Transition Diagram for StateMachine contract: +// +// NOT_INITIALIZED <- +// | | +// ↓ | +// STAKE_DEPOSITED -- +// / \ | +// ↓ ↓ | +// LIVE <- WAITING_FOR_APPROVAL +// | \ +// | ↓ +// | BEING_SLASHED +// | / +// ↓ ↓ +// EXITED +// | +// ↓ +// FULLY_WITHDRAWN +rule validatorStateTransitions(IEtherFiNode.VALIDATOR_PHASE oldPhase, IEtherFiNode.VALIDATOR_PHASE newPhase) { + bool res; + + IEtherFiNode.VALIDATOR_PHASE phaseBefore = oldPhase; + res = validatePhaseTransition(oldPhase, newPhase); // call phase instead. + IEtherFiNode.VALIDATOR_PHASE phaseAfter = newPhase; + + assert phaseAfter == NOT_INITIALIZED() => phaseBefore == NOT_INITIALIZED() || phaseBefore == STAKE_DEPOSITED() || phaseBefore == WAITING_FOR_APPROVAL(), "NOT_INITIALIZED transtion violated"; + assert phaseAfter == STAKE_DEPOSITED() => phaseBefore == NOT_INITIALIZED(), "STAKE_DEPOSITED transtion violated"; + assert phaseAfter == LIVE() => phaseBefore == STAKE_DEPOSITED() || phaseBefore == WAITING_FOR_APPROVAL(), "LIVE transtion violated"; + assert phaseAfter == EXITED() => phaseBefore == LIVE() || phaseBefore == BEING_SLASHED(), "EXITED transtion violated"; + assert phaseAfter == FULLY_WITHDRAWN() => phaseBefore == EXITED(), "FULLY_WITHDRAWN transtion violated"; + assert phaseAfter == BEING_SLASHED() => phaseBefore == LIVE(), "BEING_SLASHED transtion violated"; + assert phaseAfter == WAITING_FOR_APPROVAL() => phaseBefore == STAKE_DEPOSITED(), "WAITING_FOR_APPROVAL transtion violated"; +} + +// version is always 1 (after initialization). +invariant versionIsOne() + version() == 1; + +invariant sumAllExitedLessThanAllAssociated() + assert_uint256(numExitedValidators() + numExitRequestsByTnft()) <= numAssociatedValidators(); + +//TODO: if NOT_INITIALIZED how can be associated???? +rule registerValidatorThenUnregisteringNeverReverts(uint256 validatorId, bool enableRestaking) { + env e; + IEtherFiNodesManager.ValidatorInfo info; + require version() == 1; // required by the node manager. + require associatedValidatorIdsLengthGhost < max_uint256; // causes overflows. + requireInvariant associatedValidatorIdsLengthEqNumOfValidators(); + + registerValidator(e, validatorId, enableRestaking); + // set validator phase to IEtherFiNode.VALIDATOR_PHASE.STAKE_DEPOSITED - required by the node manager. + require info.validatorIndex == 0; // requires by the node manager. + + require (info.phase == NOT_INITIALIZED() || info.phase == FULLY_WITHDRAWN()); // requires by the node manager. + if (info.phase == FULLY_WITHDRAWN()) { + require numExitedValidators() > 0; // FULLY_WITHDRAWN can be only if exited before. + } + require info.exitRequestTimestamp == 0; // seens to be a deprecated filed in the struct. + + bool succeed = unRegisterValidator@withrevert(e, validatorId, info); + + bool didRevert = lastReverted; + + assert !didRevert; +} + +invariant associatedValidatorIdsLengthEqNumOfValidators() + associatedValidatorIdsLengthGhost == numAssociatedValidators() + { + preserved { + requireInvariant versionIsOne(); + } preserved unRegisterValidator(uint256 validatorId, IEtherFiNodesManager.ValidatorInfo info) with (env e) { + if (info.phase == FULLY_WITHDRAWN() && numAssociatedValidators() > 0) { + // TODO: is it even possible with the tool? + updateNumberOfAssociatedValidators(e, 0, 1); // done by node manager at fullWithdraw. (calls processFullWithdraw). + // associatedValidatorIdsLengthGhost = assert_uint256(associatedValidatorIdsLengthGhost - 1); // was never in this array if NOT_INITIALIZED. + } else if (info.phase == NOT_INITIALIZED() && associatedValidatorIdsLengthGhost > 0) { + updateNumberOfAssociatedValidators(e, 0, 1); // done by node manager at fullWithdraw. (calls processFullWithdraw). + } + } + preserved processFullWithdraw(uint256 validatorId) with (env e) { + if (associatedValidatorIdsLengthGhost > 0) { + associatedValidatorIdsLengthGhost = assert_uint256(associatedValidatorIdsLengthGhost - 1); // done by node manager at fullWithdraw. (calls unregister before) + } + } + } + +// numexited + num exited < numallassosiated + +// pending Gwei correlation with assosiatedValidators +// invariant pendingGweiAssociatedValidatorsCorrelation() + +// restakingObservedExitBlocks are less than current.block - only for corrcness (may cause false violations) + +// for node manager: +// no same validatorId is present/assosiated in defferent etherFiNodes +// sumAllAssociatedValidatorIds equals _numAssociatedValidators - because it is update in the manager while sumAllAssociatedValidatorIds is tracked through the node itself +// sumAllAssociatedValidatorIds equals sum of validators in a suitable PHASE. +// _numAssociatedValidators equals sum of validators in a suitable PHASE. + diff --git a/certora/specs/EtherFiNodeSetup.spec b/certora/specs/EtherFiNodeSetup.spec new file mode 100644 index 00000000..81bfa85e --- /dev/null +++ b/certora/specs/EtherFiNodeSetup.spec @@ -0,0 +1,174 @@ +methods { + // Getters: + function eigenPod() external returns (address) envfree; + function isRestakingEnabled() external returns (bool) envfree; + function version() external returns (uint16) envfree; + function _numAssociatedValidators() internal returns (uint16); + function associatedValidatorIndices(uint256) external returns (uint256) envfree; + function numExitedValidators() external returns (uint16) envfree; + function numExitRequestsByTnft() external returns (uint16) envfree; + function associatedValidatorIds(uint256) external returns (uint256) envfree; + // Track the amount of pending/completed withdrawals; + function pendingWithdrawalFromRestakingInGwei() external returns (uint64) envfree; + function completedWithdrawalFromRestakingInGwei() external returns (uint64) envfree; + function updateNumberOfAssociatedValidators(uint16, uint16) external; + + function numAssociatedValidators() external returns (uint256) envfree; + function registerValidator(uint256, bool) external; + function validatePhaseTransition(IEtherFiNode.VALIDATOR_PHASE, IEtherFiNode.VALIDATOR_PHASE) external returns (bool) envfree; + + // IEigenPodManager summaries: + function _.eigenPodManager() external => NONDET; + function _.getPod(address) external => NONDET; + function _.createPod() external => NONDET; + + // munge: + function getAssociatedValidatorIdsLength() external returns (uint256) envfree; + +} + +definition NOT_INITIALIZED() returns IEtherFiNode.VALIDATOR_PHASE = IEtherFiNode.VALIDATOR_PHASE.NOT_INITIALIZED; +definition STAKE_DEPOSITED() returns IEtherFiNode.VALIDATOR_PHASE = IEtherFiNode.VALIDATOR_PHASE.STAKE_DEPOSITED; +definition LIVE() returns IEtherFiNode.VALIDATOR_PHASE = IEtherFiNode.VALIDATOR_PHASE.LIVE; +definition EXITED() returns IEtherFiNode.VALIDATOR_PHASE = IEtherFiNode.VALIDATOR_PHASE.EXITED; +definition FULLY_WITHDRAWN() returns IEtherFiNode.VALIDATOR_PHASE = IEtherFiNode.VALIDATOR_PHASE.FULLY_WITHDRAWN; +definition BEING_SLASHED() returns IEtherFiNode.VALIDATOR_PHASE = IEtherFiNode.VALIDATOR_PHASE.BEING_SLASHED; +definition WAITING_FOR_APPROVAL() returns IEtherFiNode.VALIDATOR_PHASE = IEtherFiNode.VALIDATOR_PHASE.WAITING_FOR_APPROVAL; + +// CALL FORWARDING filtered: +definition callForwarding(method f) returns bool = + f.selector == sig:callEigenPod(bytes).selector || + f.selector == sig:forwardCall(address, bytes).selector; + +persistent ghost uint256 associatedValidatorIdsLengthGhost { + init_state axiom associatedValidatorIdsLengthGhost == 0; +} + +persistent ghost mapping(uint256 => uint256) associatedValidatorIndicesGhost { + init_state axiom forall uint256 validator . associatedValidatorIndicesGhost[validator] == 0; +} + +persistent ghost mathint sumAllAssociatedValidatorIndicesGhost { + init_state axiom sumAllAssociatedValidatorIndicesGhost == 0; + axiom sumAllAssociatedValidatorIndicesGhost >= 0; +} + +persistent ghost mapping(uint256 => uint256) associatedValidatorIdsGhost { + init_state axiom forall uint256 index . associatedValidatorIdsGhost[index] == 0; +} + +persistent ghost mathint sumAllAssociatedValidatorIds { + init_state axiom sumAllAssociatedValidatorIds == 0; + axiom sumAllAssociatedValidatorIds >= 0; +} +persistent ghost uint32 latestBlockGhost { + init_state axiom latestBlockGhost == 0; +} + +persistent ghost mapping(uint256 => uint32) restakingObservedExitBlocksGhost { + init_state axiom forall uint256 validatorId . restakingObservedExitBlocksGhost[validatorId] == 0; +} + +hook Sstore restakingObservedExitBlocks[KEY uint256 validatorId] uint32 newblock (uint32 oldBlock) { + if (newblock > latestBlockGhost) { + latestBlockGhost = newblock; + } + restakingObservedExitBlocksGhost[validatorId] = newblock; +} + +hook Sload uint32 blockNumber restakingObservedExitBlocks[KEY uint256 validatorId] { + require blockNumber == restakingObservedExitBlocksGhost[validatorId]; +} + +hook Sstore associatedValidatorIds.(offset 0) uint256 newlength (uint256 oldlength) { + require oldlength == associatedValidatorIdsLengthGhost; + associatedValidatorIdsLengthGhost = newlength; +} + +hook Sload uint256 length associatedValidatorIds.(offset 0) { + require length == associatedValidatorIdsLengthGhost; +} + +hook Sstore associatedValidatorIndices[KEY uint256 validator] uint256 newIndecies (uint256 oldIndecies) { + associatedValidatorIndicesGhost[validator] = newIndecies; + sumAllAssociatedValidatorIndicesGhost = sumAllAssociatedValidatorIndicesGhost + newIndecies - oldIndecies; +} + +hook Sload uint256 indecies associatedValidatorIndices[KEY uint256 validator] { + require indecies == associatedValidatorIndicesGhost[validator]; +} + +hook Sstore associatedValidatorIds[INDEX uint256 index] uint256 newValidator (uint256 oldValidator) { + if (newValidator == 0 && oldValidator != 0) { + sumAllAssociatedValidatorIds = sumAllAssociatedValidatorIds - 1; + } else if (newValidator != 0 && oldValidator == 0) { + sumAllAssociatedValidatorIds = sumAllAssociatedValidatorIds + 1; + } + associatedValidatorIdsGhost[index] = newValidator; +} + +hook Sload uint256 validator associatedValidatorIds[INDEX uint256 index] { + require validator == associatedValidatorIdsGhost[index]; +} + +invariant mirrorLength() + associatedValidatorIdsLengthGhost == getAssociatedValidatorIdsLength(); + +invariant validatorIndeciesLessThanLength(uint256 validatorId, uint256 index) + forall uint256 validator . associatedValidatorIndicesGhost[validator] <= associatedValidatorIdsLengthGhost; + +invariant validatorPastLengthAreNullified() + forall uint256 index . index > associatedValidatorIdsLengthGhost => associatedValidatorIdsGhost[index] == 0 + { + preserved registerValidator(uint256 validatorId, bool redtskingEnabled) with (env e) { + require validatorId != 0; + } + } + +// invariant mirrorIntegrity(uint256 index) +// index < associatedValidatorIdsLengthGhost => +// associatedValidatorIndicesGhost[associatedValidatorIdsGhost[index]] == index && +// associatedValidatorIdsGhost[associatedValidatorIndicesGhost[validator]] == validator; + +invariant validatorIndeciesValidaorIdMirror() + forall uint256 validatorId . associatedValidatorIndicesGhost[validatorId] != 0 => + associatedValidatorIdsGhost[associatedValidatorIndicesGhost[validatorId]] == validatorId; + +invariant validatorIdNeverZero() + forall uint256 index . index < associatedValidatorIdsLengthGhost => associatedValidatorIdsGhost[index] != 0 + { + preserved registerValidator(uint256 validatorId, bool redtskingEnabled) with (env e) { + // validatorId starts from 1. + require validatorId != 0; + } + } + +// invariant validatorIndeciesValidaorIdMirror() +// forall uint256 validatorId . associatedValidatorIndices(validatorId) != 0 => +// associatedValidatorIds(associatedValidatorIndices(validatorId)) == validatorId; + +// it is not proven and might be allowed by the system but it helps to prove properties on the EtherFiNode. +// invariant validatorIdsAreUnique(uint256 validatorId) if there are two different indexes then their validatorId is different (if indexes less than length) +// (validatorId != 0 && associatedValidatorIndicesGhost[validatorId] == 0) => (forall uint256 index . associatedValidatorIdsGhost[index] != validatorId); + +invariant blockNumberValidity(uint32 blockNumber) + blockNumber >= latestBlockGhost + { + preserved with (env e) { + require e.block.number == blockNumber; + } + } + +invariant validatorIdsAreUnique() + forall uint256 index1 . forall uint256 index2 . + (index1 != index2 && index1 < associatedValidatorIdsLengthGhost && index2 < associatedValidatorIdsLengthGhost) => + associatedValidatorIdsGhost[index1] != associatedValidatorIdsGhost[index2] + { + preserved with (env e) { + requireInvariant validatorIdNeverZero(); + requireInvariant validatorPastLengthAreNullified(); + } + } + + + // אם אינדקס קטן אז שונה מאפס ואם גדול אז שווה לאפס diff --git a/certora/specs/EtherFiNodesManager.spec b/certora/specs/EtherFiNodesManager.spec index 15b5dcab..8e3cd60e 100644 --- a/certora/specs/EtherFiNodesManager.spec +++ b/certora/specs/EtherFiNodesManager.spec @@ -28,38 +28,52 @@ function ghostGetValidatorPhase(uint256 validatorId) returns uint8 { // DEPRECATED_READY_FOR_DEPOSIT,9 // } -// Verify state diafram from documentation. -// State Transition Diagram for StateMachine contract: -// -// NOT_INITIALIZED <- -// | | -// ↓ | -// STAKE_DEPOSITED -- -// / \ | -// ↓ ↓ | -// LIVE <- WAITING_FOR_APPROVAL -// | \ -// | ↓ -// | BEING_SLASHED -// | / -// ↓ ↓ -// EXITED -// | -// ↓ -// FULLY_WITHDRAWN -rule validatorStateTransitions(method f, uint256 validatorId) { - env e; - calldataarg args; +// definition NOT_INITIALIZED() returns uint8 = IEtherFiNode.VALIDATOR_PHASE.NOT_INITIALIZED; +// definition STAKE_DEPOSITED() returns uint8 = IEtherFiNode.VALIDATOR_PHASE.STAKE_DEPOSITED; +// definition NOT_INITIALIZED() returns uint8 = IEtherFiNode.VALIDATOR_PHASE.NOT_INITIALIZED; +// definition NOT_INITIALIZED() returns uint8 = IEtherFiNode.VALIDATOR_PHASE.NOT_INITIALIZED; +// definition NOT_INITIALIZED() returns uint8 = IEtherFiNode.VALIDATOR_PHASE.NOT_INITIALIZED; - uint8 phaseBefore = validatorPhase[validatorId]; - f(e, args); - uint8 phaseAfter = validatorPhase[validatorId]; +// // Verify state diafram from documentation. +// // State Transition Diagram for StateMachine contract: +// // +// // NOT_INITIALIZED <- +// // | | +// // ↓ | +// // STAKE_DEPOSITED -- +// // / \ | +// // ↓ ↓ | +// // LIVE <- WAITING_FOR_APPROVAL +// // | \ +// // | ↓ +// // | BEING_SLASHED +// // | / +// // ↓ ↓ +// // EXITED +// // | +// // ↓ +// // FULLY_WITHDRAWN +// rule validatorStateTransitions(method f, uint256 validatorId) { +// env e; +// calldataarg args; +// bool res; - assert phaseAfter == 0 => phaseBefore == 0 || phaseBefore == 1 || phaseBefore == 8, "NOT_INITIALIZED transtion violated"; - assert phaseAfter == 1 => phaseBefore == 0, "STAKE_DEPOSITED transtion violated"; - assert phaseAfter == 2 => phaseBefore == 1 || phaseBefore == 8, "LIVE transtion violated"; - assert phaseAfter == 3 => phaseBefore == 2 || phaseBefore == 6, "EXITED transtion violated"; - assert phaseAfter == 4 => phaseBefore == 3, "FULLY_WITHDRAWN transtion violated"; - assert phaseAfter == 6 => phaseBefore == 2, "BEING_SLASHED transtion violated"; - assert phaseAfter == 8 => phaseBefore == 1, "WAITING_FOR_APPROVAL transtion violated"; -} +// uint8 phaseBefore = validatorPhase[validatorId]; +// res = f(e, args); // call phase instead. +// uint8 phaseAfter = validatorPhase[validatorId]; + +// assert phaseAfter == 0 => phaseBefore == 0 || phaseBefore == 1 || phaseBefore == 8, "NOT_INITIALIZED transtion violated"; +// assert phaseAfter == 1 => phaseBefore == 0, "STAKE_DEPOSITED transtion violated"; +// assert phaseAfter == 2 => phaseBefore == 1 || phaseBefore == 8, "LIVE transtion violated"; +// assert phaseAfter == 3 => phaseBefore == 2 || phaseBefore == 6, "EXITED transtion violated"; +// assert phaseAfter == 4 => phaseBefore == 3, "FULLY_WITHDRAWN transtion violated"; +// assert phaseAfter == 6 => phaseBefore == 2, "BEING_SLASHED transtion violated"; +// assert phaseAfter == 8 => phaseBefore == 1, "WAITING_FOR_APPROVAL transtion violated"; +// } + + +// methods effecting only one Node +// dosnt fail when must succeed +// who changes the eth balance of the contract +// amount of tnft / bnft must eq the amount of validator in phase live or waiting for approval. +// no different node should share the same validator id. From 3f55802b8cd784487fca19a22ae2b6f00de9f72c Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Mon, 16 Sep 2024 10:24:08 +0300 Subject: [PATCH 14/26] auction manager update --- certora/specs/AuctionManager.spec | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) diff --git a/certora/specs/AuctionManager.spec b/certora/specs/AuctionManager.spec index cabdc0ae..bb735715 100644 --- a/certora/specs/AuctionManager.spec +++ b/certora/specs/AuctionManager.spec @@ -50,12 +50,6 @@ invariant activeBidsSolvency() } } -// the sum of all used keys equals num of bids. -// invariant numOfAllUsedKeysEqNumOfBids() {} - -// chack for all bids to see if the key index is unique per user. / not same user with same keyIndex on different bids: -// rule bidderPubKeyIndexIsUniqePerUser() {} - rule bidImmutability(method f, uint256 bid_id) filtered {f -> !isFilteredFunc(f)} { env e; calldataarg args; @@ -85,6 +79,7 @@ invariant alwaysInitialized() currentContract._initialized == max_uint8 filtered {f -> !isFilteredFunc(f)} +/// @title createBid works as intended. rule integrityOfCreateBid(uint256 _bidSize, uint256 _bidAmountPerBid) { env e; uint256 newBidId; @@ -115,8 +110,8 @@ rule integrityOfCreateBid(uint256 _bidSize, uint256 _bidAmountPerBid) { // trivial due to requires: assert msgValue == _bidSize * _bidAmountPerBid, "function should have reverted"; // number of bids update correctly - assert numberOfBidsAfter == numberOfBidsBefore + _bidSize, "ammount of bids updated incorrectly"; - assert numberOfActiveBidsAfter == numberOfActiveBidsBefore + _bidSize, "ammount of active bids updated incorrectly"; + assert numberOfBidsAfter == numberOfBidsBefore + _bidSize, "amount of bids updated incorrectly"; + assert numberOfActiveBidsAfter == numberOfActiveBidsBefore + _bidSize, "amount of active bids updated incorrectly"; assert senderLastKeyIndex == senderFirstKeyIndex + _bidSize, "amount of used keys updated incorrectly"; // the right bids were added: assert amount == _bidAmountPerBid; @@ -125,6 +120,3 @@ rule integrityOfCreateBid(uint256 _bidSize, uint256 _bidAmountPerBid) { assert isActive; } -// rule integrityOfCancelBid(uint256 bidId) { -// env e; -// } From 13e0a1f3db74dfb24aa58565aad9269a5699bd62 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Mon, 16 Sep 2024 19:28:07 +0300 Subject: [PATCH 15/26] AuctionManager --- certora/config/AuctionManager.conf | 2 +- certora/specs/AuctionManager.spec | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/certora/config/AuctionManager.conf b/certora/config/AuctionManager.conf index 59921a12..3cf27bff 100644 --- a/certora/config/AuctionManager.conf +++ b/certora/config/AuctionManager.conf @@ -15,5 +15,5 @@ "optimistic_fallback": true, "loop_iter": "3", "solc": "solc8.24", - "msg": "all AuctionManager", + "msg": "AuctionManager", } diff --git a/certora/specs/AuctionManager.spec b/certora/specs/AuctionManager.spec index bb735715..3128603e 100644 --- a/certora/specs/AuctionManager.spec +++ b/certora/specs/AuctionManager.spec @@ -26,17 +26,17 @@ definition isFilteredFunc(method f) returns bool = ( f.selector == sig:upgradeToAndCall(address, bytes).selector ); -// numberOfActiveBids equals the sum of active bids. +/// @title numberOfActiveBids equals the sum of active bids. invariant numberOfActiveBidsCorrect() sum_of_active_bids == to_mathint(numberOfActiveBids()) filtered {f -> !isFilteredFunc(f)} -// numberOfBids equals the sum of all bids. +/// @title numberOfBids equals the sum of all bids. invariant numberOfBidsEqTheSumOfAllBids() sum_of_bids == to_mathint(numberOfBids()) filtered {f -> !isFilteredFunc(f) && f.selector != sig:initialize(address).selector} -// solvency invariant - contract should hold atleast sumOfAllActiveBidAmounts amount of eth. +/// @title solvency invariant - contract should hold atleast sumOfAllActiveBidAmounts amount of eth. invariant activeBidsSolvency() to_mathint(nativeBalances[currentContract]) >= sum_of_all_active_bids_amounts filtered {f -> !isFilteredFunc(f)} @@ -50,6 +50,7 @@ invariant activeBidsSolvency() } } +/// @title once a bid is set, the only field that can be changed is isActive field. rule bidImmutability(method f, uint256 bid_id) filtered {f -> !isFilteredFunc(f)} { env e; calldataarg args; @@ -74,7 +75,7 @@ rule bidImmutability(method f, uint256 bid_id) filtered {f -> !isFilteredFunc(f) assert bidderAddressBefore == bidderAddressAfter, "bidder address was changed"; } -/// @title The contact is set as initialized in the constructor -- seems a bug? +/// @title The contact is set as initialized in the constructor. invariant alwaysInitialized() currentContract._initialized == max_uint8 filtered {f -> !isFilteredFunc(f)} From 0aacea577f01cb0bd7c75f6eb92c6fca26008c0c Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Mon, 16 Sep 2024 19:31:16 +0300 Subject: [PATCH 16/26] Auction Manager Setup remove redundant --- certora/specs/AuctionManageSetup.spec | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/certora/specs/AuctionManageSetup.spec b/certora/specs/AuctionManageSetup.spec index 1751ac90..b2fb79a2 100644 --- a/certora/specs/AuctionManageSetup.spec +++ b/certora/specs/AuctionManageSetup.spec @@ -2,7 +2,6 @@ methods { function _.upgradeToAndCall(address,bytes) external => NONDET; } -/// Is persistent because it mirrors the PoolManager storage. persistent ghost mapping(uint256 => uint256) bids_amount { init_state axiom forall uint256 bid_id . bids_amount[bid_id] == 0; } @@ -15,28 +14,17 @@ ghost mathint sum_of_active_bids { init_state axiom sum_of_active_bids == 0; } -ghost mathint sum_of_all_bids_amounts { - init_state axiom sum_of_all_bids_amounts == 0; -} - ghost mathint sum_of_all_active_bids_amounts { init_state axiom sum_of_all_active_bids_amounts == 0; } -ghost uint256 latest_bid_id; - ghost mapping(uint256 => bool) bids_is_active { init_state axiom forall uint256 bid_id . bids_is_active[bid_id] == false; } -ghost mapping(address => uint256) user_last_bid_id_index { - init_state axiom forall address user . user_last_bid_id_index[user] == 0; -} - hook Sstore bids[KEY uint256 bid_id].amount uint256 new_amount (uint256 old_amount) { bids_amount[bid_id] = new_amount; sum_of_bids = sum_of_bids + 1; - sum_of_all_bids_amounts = sum_of_all_bids_amounts + new_amount; } hook Sload uint256 _amount bids[KEY uint256 bid_id].amount { From 718c8b0b5145e22ae66477956cf630ba73f0d64c Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Mon, 16 Sep 2024 19:34:39 +0300 Subject: [PATCH 17/26] EETH update --- certora/specs/EETH.spec | 16 +--------------- 1 file changed, 1 insertion(+), 15 deletions(-) diff --git a/certora/specs/EETH.spec b/certora/specs/EETH.spec index c89fbe0c..0c069f8f 100644 --- a/certora/specs/EETH.spec +++ b/certora/specs/EETH.spec @@ -39,18 +39,6 @@ invariant totalSharesIsSumOfShares() f -> f.selector != sig:upgradeToAndCall(address,bytes).selector } -/// @title The sum of shares of two users is not greater than total shares -invariant sumOfTwo(address user1, address user2) - shares(user1) + shares(user2) <= sumOfShares - filtered { - f -> f.selector != sig:upgradeToAndCall(address,bytes).selector - } - { - preserved { - requireInvariant totalSharesIsSumOfShares(); - } - } - /** Verify that there is no fee on transfer. **/ @@ -151,10 +139,8 @@ rule TransferFromDoesntChangeOtherBalance(address from, address to, uint256 amou assert balanceBefore == shares(other); } +// More ideas for rules for EtherFi to implement: // rule mintMonotonicity() {} - // rule mintAccumulativity() {} - // rule burnMonotonicity() {} - // rule burnAccumulativity() {} From f011de70ea67ed5bb579e78039f101379271f010 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Mon, 16 Sep 2024 19:36:24 +0300 Subject: [PATCH 18/26] nft dispatch update --- certora/specs/nftDispach.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/nftDispach.spec b/certora/specs/nftDispach.spec index d8837116..c4628fd5 100644 --- a/certora/specs/nftDispach.spec +++ b/certora/specs/nftDispach.spec @@ -15,7 +15,7 @@ methods { // BNFT: function _.burnFromWithdrawal(uint256) external => DISPATCHER(true); - function _.initialize() external => DISPATCHER(true); + // function _.initialize() external => DISPATCHER(true); function _.initializeOnUpgrade(address) external => DISPATCHER(true); function _.mint(address, uint256) external => DISPATCHER(true); function _.burnFromCancelBNftFlow(uint256) external => DISPATCHER(true); From 46135db2e1f945bd9fb1afe9a40351830c6cb0e9 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Mon, 16 Sep 2024 19:47:02 +0300 Subject: [PATCH 19/26] update staking manager --- certora/config/StakingManager.conf | 5 +- certora/specs/EtherFiNodesManager.spec | 64 +---------- certora/specs/StakingManager.spec | 143 ------------------------- certora/specs/nftDispach.spec | 4 +- 4 files changed, 5 insertions(+), 211 deletions(-) diff --git a/certora/config/StakingManager.conf b/certora/config/StakingManager.conf index 76987949..9b03fe6d 100644 --- a/certora/config/StakingManager.conf +++ b/certora/config/StakingManager.conf @@ -22,10 +22,9 @@ "optimistic_loop": true, "optimistic_fallback": true, "optimistic_hashing": true, - // "parametric_contracts":["StakingManager"], + "parametric_contracts":["StakingManager", "AuctionManager"], "build_cache": true, "loop_iter": "3", "solc": "solc8.24", - "msg": "all StakingManager", - "rule": ["whoLeaveEth"], + "msg": "StakingManager", } diff --git a/certora/specs/EtherFiNodesManager.spec b/certora/specs/EtherFiNodesManager.spec index 8e3cd60e..975dae06 100644 --- a/certora/specs/EtherFiNodesManager.spec +++ b/certora/specs/EtherFiNodesManager.spec @@ -3,6 +3,7 @@ methods { function _.phase(uint256 _validatorId) external => ghostGetValidatorPhase(_validatorId) expect uint8; } +// Summaries for staking manager used instead of linking the contract itself. persistent ghost mapping(uint256 => uint8) validatorPhase { init_state axiom forall uint256 validatorId . validatorPhase[validatorId] == 0; } @@ -14,66 +15,3 @@ function ghostSetValidatorPhase(uint256 validatorId, uint8 phase) { function ghostGetValidatorPhase(uint256 validatorId) returns uint8 { return validatorPhase[validatorId]; } - -// enum VALIDATOR_PHASE { -// NOT_INITIALIZED,0 -// STAKE_DEPOSITED,1 -// LIVE,2 -// EXITED,3 -// FULLY_WITHDRAWN,4 -// DEPRECATED_CANCELLED,5 -// BEING_SLASHED,6 -// DEPRECATED_EVICTED,7 -// WAITING_FOR_APPROVAL,8 -// DEPRECATED_READY_FOR_DEPOSIT,9 -// } - -// definition NOT_INITIALIZED() returns uint8 = IEtherFiNode.VALIDATOR_PHASE.NOT_INITIALIZED; -// definition STAKE_DEPOSITED() returns uint8 = IEtherFiNode.VALIDATOR_PHASE.STAKE_DEPOSITED; -// definition NOT_INITIALIZED() returns uint8 = IEtherFiNode.VALIDATOR_PHASE.NOT_INITIALIZED; -// definition NOT_INITIALIZED() returns uint8 = IEtherFiNode.VALIDATOR_PHASE.NOT_INITIALIZED; -// definition NOT_INITIALIZED() returns uint8 = IEtherFiNode.VALIDATOR_PHASE.NOT_INITIALIZED; - -// // Verify state diafram from documentation. -// // State Transition Diagram for StateMachine contract: -// // -// // NOT_INITIALIZED <- -// // | | -// // ↓ | -// // STAKE_DEPOSITED -- -// // / \ | -// // ↓ ↓ | -// // LIVE <- WAITING_FOR_APPROVAL -// // | \ -// // | ↓ -// // | BEING_SLASHED -// // | / -// // ↓ ↓ -// // EXITED -// // | -// // ↓ -// // FULLY_WITHDRAWN -// rule validatorStateTransitions(method f, uint256 validatorId) { -// env e; -// calldataarg args; -// bool res; - -// uint8 phaseBefore = validatorPhase[validatorId]; -// res = f(e, args); // call phase instead. -// uint8 phaseAfter = validatorPhase[validatorId]; - -// assert phaseAfter == 0 => phaseBefore == 0 || phaseBefore == 1 || phaseBefore == 8, "NOT_INITIALIZED transtion violated"; -// assert phaseAfter == 1 => phaseBefore == 0, "STAKE_DEPOSITED transtion violated"; -// assert phaseAfter == 2 => phaseBefore == 1 || phaseBefore == 8, "LIVE transtion violated"; -// assert phaseAfter == 3 => phaseBefore == 2 || phaseBefore == 6, "EXITED transtion violated"; -// assert phaseAfter == 4 => phaseBefore == 3, "FULLY_WITHDRAWN transtion violated"; -// assert phaseAfter == 6 => phaseBefore == 2, "BEING_SLASHED transtion violated"; -// assert phaseAfter == 8 => phaseBefore == 1, "WAITING_FOR_APPROVAL transtion violated"; -// } - - -// methods effecting only one Node -// dosnt fail when must succeed -// who changes the eth balance of the contract -// amount of tnft / bnft must eq the amount of validator in phase live or waiting for approval. -// no different node should share the same validator id. diff --git a/certora/specs/StakingManager.spec b/certora/specs/StakingManager.spec index 80e96416..6aa2d0bb 100644 --- a/certora/specs/StakingManager.spec +++ b/certora/specs/StakingManager.spec @@ -36,9 +36,6 @@ methods { function auctionManager.processAuctionFeeTransfer(uint256) external => NONDET; } -use invariant sumAllTNFTEqSumAllTNFTBalances; -use invariant sumAllBNFTEqSumAllBNFTBalances; - // Functions filtered out since they use `delegatecall`. definition isFilteredFunc(method f) returns bool = ( f.selector == sig:upgradeToAndCall(address, bytes).selector @@ -114,126 +111,6 @@ rule integrityOfBatchCancelDeposit(uint256 validatorId, address caller) { assert phasePre == 8 => bnft.ownerOf(e, validatorId) == 0 && tnft.ownerOf(e, validatorId) == 0, "wrong nfts were burned"; } -rule batchCancelDepositFR(method f, uint256 validatorId, address caller) - filtered { f -> !isFilteredFunc(f) - && f.selector != sig:pauseContract().selector - || f.selector != sig:instantiateEtherFiNode(bool).selector - || f.selector != sig:initialize(address,address).selector } { - env e; - env eFr; - calldataarg args; - require eFr.msg.sender != e.msg.sender; - require e.msg.sender != currentContract; - require e.msg.sender != auctionManager; - require eFr.msg.sender != currentContract; - // require eFr.msg.sender != auctionManager; - require e.msg.sender != 0; - require eFr.msg.sender != 0; - uint256[] validatorIds = [validatorId]; - - storage initState = lastStorage; - - batchCancelDeposit(e, validatorIds, caller); - - f(eFr, args) at initState; - - batchCancelDeposit@withrevert(e, validatorIds, caller); - - bool didRvert = lastReverted; - - assert !didRvert; -} - -rule batchDepositFR(method f) - filtered { f -> !isFilteredFunc(f) - && f.selector != sig:pauseContract().selector - || f.selector != sig:instantiateEtherFiNode(bool).selector - || f.selector != sig:initialize(address,address).selector } { - env e; - env eFr; - calldataarg args; - require eFr.msg.sender != e.msg.sender; - require e.msg.sender != currentContract; - require e.msg.sender != auctionManager; - require eFr.msg.sender != currentContract; - // require eFr.msg.sender != auctionManager; - require e.msg.sender != 0; - require eFr.msg.sender != 0; - calldataarg specificArgs; - - storage initState = lastStorage; - - batchDepositWithBidIds(e, specificArgs); - - f(eFr, args) at initState; - - batchDepositWithBidIds@withrevert(e, specificArgs); - - bool didRvert = lastReverted; - - assert !didRvert; -} - -rule batchRegisterValidatorsFR(method f, uint256 bidID) - filtered { f -> !isFilteredFunc(f) - && f.selector != sig:pauseContract().selector - || f.selector != sig:instantiateEtherFiNode(bool).selector - || f.selector != sig:initialize(address,address).selector } { - env e; - env eFr; - calldataarg specificArgs; - calldataarg args; - require eFr.msg.sender != e.msg.sender; - require e.msg.sender != currentContract; - require e.msg.sender != auctionManager; - require eFr.msg.sender != currentContract; - // require eFr.msg.sender != auctionManager; - require e.msg.sender != 0; - require eFr.msg.sender != 0; - - storage initState = lastStorage; - - batchRegisterValidators(e, specificArgs); - - f(eFr, args) at initState; - - batchRegisterValidators@withrevert(e, specificArgs); - - bool didRvert = lastReverted; - - assert !didRvert; -} - -rule batchApproveRegistrationFR(method f, uint256 bidID) - filtered { f -> !isFilteredFunc(f) - && f.selector != sig:pauseContract().selector - || f.selector != sig:instantiateEtherFiNode(bool).selector - || f.selector != sig:initialize(address,address).selector } { - env e; - env eFr; - calldataarg args; - calldataarg specificArgs; - require eFr.msg.sender != e.msg.sender; - require e.msg.sender != currentContract; - require e.msg.sender != auctionManager; - require eFr.msg.sender != currentContract; - // require eFr.msg.sender != auctionManager; - require e.msg.sender != 0; - require eFr.msg.sender != 0; - - storage initState = lastStorage; - - batchApproveRegistration(e, specificArgs); - - f(eFr, args) at initState; - - batchApproveRegistration@withrevert(e, specificArgs); - - bool didRvert = lastReverted; - - assert !didRvert; -} - rule integrityOfBatchRegisterValidators(uint256 validatorId) { env e; require e.msg.sender != currentContract; @@ -267,23 +144,3 @@ rule integrityOfBatchRegisterValidators(uint256 validatorId) { assert tnft.ownerOf(e, validatorId) == tNftRecipient, "tnft was minted for the wrong user"; assert bnft.ownerOf(e, validatorId) == bNftRecipient, "bnft was minted for the wrong user"; } - -rule integrityOfBatchApproveRegistration(uint256 validatorId) { - env e; - uint256 val = e.msg.value; - uint256[] validatorIds = [validatorId]; - bytes[] pubKey; - bytes[] signature; - bytes32[] depositDataRootApproval; - - // LiquidityPool requirements: - require validatorIds.length == pubKey.length; - require validatorIds.length == signature.length; - - batchApproveRegistration(e, validatorIds, pubKey, signature, depositDataRootApproval); - - uint8 _validatorPhase = validatorPhase[validatorId]; - - // assert validator phase: - satisfy true; -} diff --git a/certora/specs/nftDispach.spec b/certora/specs/nftDispach.spec index c4628fd5..9337dcc6 100644 --- a/certora/specs/nftDispach.spec +++ b/certora/specs/nftDispach.spec @@ -98,10 +98,10 @@ hook Sload uint256 count bnft._balances[KEY address owner] { require count == bntBalances[owner]; } -// amount of tnfts with owner equals the sum of every tnft owner balance. +// amount of tnfts with owner equals the sum of every tnft owner balance. - should fail invariant sumAllTNFTEqSumAllTNFTBalances() sumAllTNFTBalances == sumAllTNFT; -// amount of bnfts with owner equals the sum of every bnft owner balance. +// amount of bnfts with owner equals the sum of every bnft owner balance. - should fail invariant sumAllBNFTEqSumAllBNFTBalances() sumAllBNFTBalances == sumAllBNFT; From 4eb3a2f1584bedb43966ba6e9bcc6b3a490661cb Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Mon, 16 Sep 2024 19:54:03 +0300 Subject: [PATCH 20/26] add oracle and remove redundant --- certora/specs/BNFT.spec | 20 ---------------- certora/specs/EtherFiOracle.spec | 23 ------------------ certora/specs/TNFT.spec | 41 -------------------------------- 3 files changed, 84 deletions(-) delete mode 100644 certora/specs/BNFT.spec delete mode 100644 certora/specs/TNFT.spec diff --git a/certora/specs/BNFT.spec b/certora/specs/BNFT.spec deleted file mode 100644 index 4b84375b..00000000 --- a/certora/specs/BNFT.spec +++ /dev/null @@ -1,20 +0,0 @@ -methods { - // IERC721Upgradeable: - function balanceOf(address) external returns (uint256) envfree; - function ownerOf(uint256) external returns (address) envfree; - function safeTransferFrom(address, address, uint256, bytes) external; - function safeTransferFrom(address, address, uint256) external; - function transferFrom(address, address, uint256) external; - function approve(address, uint256) external; - function setApprovalForAll(address, bool) external; - function getApproved(uint256 tokenId) external view returns (address operator); - function isApprovedForAll(address, address) external returns (bool) envfree; - - // BNFT: - function burnFromWithdrawal(uint256) external; - function initialize() external; - function initializeOnUpgrade(address) external; - function mint(address, uint256) external; - function burnFromCancelBNftFlow(uint256) external; - function upgradeTo(address) external; -} diff --git a/certora/specs/EtherFiOracle.spec b/certora/specs/EtherFiOracle.spec index e2a16d21..59f021f6 100644 --- a/certora/specs/EtherFiOracle.spec +++ b/certora/specs/EtherFiOracle.spec @@ -69,23 +69,6 @@ invariant numActiveIsSumActive() } } - -// active members <= total members -//unable to prove this invariant because a lot of other invariants required -// invariant invariantTotalMoreThanActive(address _user) -// currentContract.numActiveCommitteeMembers <= currentContract.numCommitteeMembers -// filtered { -// f -> f.selector != (sig:upgradeToAndCall(address,bytes).selector) -// } -// { -// preserved { -// requireInvariant testActiveCommitteeMembersEnabled(_user); -// requireInvariant numMembersIsSumMembers(); -// requireInvariant numActiveIsSumActive(); -// require(currentContract.numCommitteeMembers > 0); -// } -// } - //consensus can only be reach if report is agreed by quorum size invariant invariantConsensusNotReached(bytes32 _reportHash) currentContract.consensusStates[_reportHash].support < currentContract.quorumSize => !currentContract.consensusStates[_reportHash].consensusReached @@ -146,7 +129,6 @@ rule testMemberCannotSubmitTwice() { assert lastReverted; } - //When publishing a report the count only increases 1 rule testHashUpdatedCorrectly(IEtherFiOracle.OracleReport _report) { env e; @@ -174,8 +156,3 @@ rule testingPublishingReport(IEtherFiOracle.OracleReport report) { submitReport(e, report); assert (currentContract.committeeMemberStates[e.msg.sender].enabled == true) && (currentContract.committeeMemberStates[e.msg.sender].registered == true); } - -/*notes from rules --what happens if we decrease quorum size submit next report --logic is funky when we change quorum size -*/ diff --git a/certora/specs/TNFT.spec b/certora/specs/TNFT.spec deleted file mode 100644 index 14c0e90c..00000000 --- a/certora/specs/TNFT.spec +++ /dev/null @@ -1,41 +0,0 @@ -methods { - // IERC721Upgradeable: - function balanceOf(address) external returns (uint256) envfree; - function ownerOf(uint256) external returns (address) envfree; - function safeTransferFrom(address, address, uint256, bytes) external; - function safeTransferFrom(address, address, uint256) external; - function transferFrom(address, address, uint256) external; - function approve(address, uint256) external; - function setApprovalForAll(address, bool) external; - function getApproved(uint256 tokenId) external view returns (address operator); - function isApprovedForAll(address, address) external returns (bool) envfree; - - // TNFT: - function burnFromWithdrawal(uint256) external; - function initialize() external; - function initializeOnUpgrade(address) external; - function mint(address, uint256) external; - function burnFromCancelBNftFlow(uint256) external; - function upgradeTo(address) external; -} - -ghost mapping(uint256 => address) owners { - init_state axiom forall uint256 id . owners[id] == 0; -} - -ghost mathint sumAllTNFT { - init_state axiom sumAllTNFT == 0; -} - -hook Sstore _owners[KEY uint256 id] address newOwner (address oldOwner) { - if(oldOwner == 0 && newOwner != 0) { - sumAllTNFT = sumAllTNFT + 1; - } else if(newOwner == 0 && oldOwner != 0) { - sumAllTNFT = sumAllTNFT 1 1; - } - owners[id] = newOwner; -} - -hook Sload address owner _owners[KEY uint256 id] { - require owner == owners[id]; -} From c54a0be03c1079310fe292e25a859aab577676ad Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Mon, 16 Sep 2024 19:55:41 +0300 Subject: [PATCH 21/26] add EtherFi interface --- certora/specs/EtherFiNodeInterface.spec | 47 +++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 certora/specs/EtherFiNodeInterface.spec diff --git a/certora/specs/EtherFiNodeInterface.spec b/certora/specs/EtherFiNodeInterface.spec new file mode 100644 index 00000000..84bd6616 --- /dev/null +++ b/certora/specs/EtherFiNodeInterface.spec @@ -0,0 +1,47 @@ +methods { + function _.numAssociatedValidators() external => DISPATCHER(true); + function _.numExitRequestsByTnft() external => DISPATCHER(true); + function _.numExitedValidators() external => DISPATCHER(true); + function _.version() external => DISPATCHER(true); + function _.eigenPod() external => DISPATCHER(true); + function _.calculateTVL(uint256, IEtherFiNodesManager.ValidatorInfo, IEtherFiNodesManager.RewardsSplit, bool) external => DISPATCHER(true); + function _.getNonExitPenalty(uint32, uint32) external => DISPATCHER(true); + function _.getRewardsPayouts(uint32, IEtherFiNodesManager.RewardsSplit) external => DISPATCHER(true); + function _.getFullWithdrawalPayouts(IEtherFiNodesManager.ValidatorInfo, IEtherFiNodesManager.RewardsSplit) external => DISPATCHER(true); + function _.associatedValidatorIds(uint256) external => DISPATCHER(true); + function _.associatedValidatorIndices(uint256) external => DISPATCHER(true); + function _.validatePhaseTransition(IEtherFiNode.VALIDATOR_PHASE, IEtherFiNode.VALIDATOR_PHASE) external => DISPATCHER(true); + + function _.DEPRECATED_exitRequestTimestamp() external => DISPATCHER(true); + function _.DEPRECATED_exitTimestamp() external => DISPATCHER(true); + function _.DEPRECATED_phase() external => DISPATCHER(true); + + // Non-VIEW functions + function _.initialize(address) external => DISPATCHER(true); + function _.DEPRECATED_claimDelayedWithdrawalRouterWithdrawals(uint256) external => DISPATCHER(true); + function _.createEigenPod() external => DISPATCHER(true); + function _.isRestakingEnabled() external => DISPATCHER(true); + function _.processNodeExit(uint256) external => DISPATCHER(true); + function _.processFullWithdraw(uint256) external => DISPATCHER(true); + function _.queueEigenpodFullWithdrawal() external => DISPATCHER(true); + function _.completeQueuedWithdrawals(IDelegationManager.Withdrawal[], uint256[], bool) external => DISPATCHER(true); + function _.completeQueuedWithdrawal(IDelegationManager.Withdrawal, uint256, bool) external => DISPATCHER(true); + function _.updateNumberOfAssociatedValidators(uint16, uint16) external => DISPATCHER(true); + function _.updateNumExitedValidators(uint16, uint16) external => DISPATCHER(true); + function _.registerValidator(uint256, bool) external => DISPATCHER(true); + function _.unRegisterValidator(uint256, IEtherFiNodesManager.ValidatorInfo) external => DISPATCHER(true); + function _.splitBalanceInExecutionLayer() external => DISPATCHER(true); + function _.totalBalanceInExecutionLayer() external => DISPATCHER(true); + function _.withdrawableBalanceInExecutionLayer() external => DISPATCHER(true); + function _.updateNumExitRequests(uint16, uint16) external => DISPATCHER(true); + function _.migrateVersion(uint256, IEtherFiNodesManager.ValidatorInfo) external => DISPATCHER(true); + // EigenPod function: + function _.startCheckpoint(bool) external => NONDET; + function _.setProofSubmitter(address) external => NONDET; + function _.callEigenPod(bytes) external => NONDET; + function _.forwardCall(address, bytes) external => NONDET; + + function _.withdrawFunds(address,uint256,address,uint256,address,uint256,address,uint256) external => DISPATCHER(true); + + function _.moveFundsToManager(uint256) external => DISPATCHER(true); +} \ No newline at end of file From d361f5a29c838152007c3a92d8397baaa88e45ae Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Wed, 18 Sep 2024 15:43:54 +0300 Subject: [PATCH 22/26] update etherfi node spec --- certora/config/EtherFiNode.conf | 2 - certora/specs/EtherFiNode.spec | 95 ++++----------------- certora/specs/EtherFiNodeSetup.spec | 126 ++++++++++++---------------- 3 files changed, 67 insertions(+), 156 deletions(-) diff --git a/certora/config/EtherFiNode.conf b/certora/config/EtherFiNode.conf index 74732ad9..1a493d72 100644 --- a/certora/config/EtherFiNode.conf +++ b/certora/config/EtherFiNode.conf @@ -12,10 +12,8 @@ "optimistic_loop": true, "optimistic_fallback": true, "optimistic_hashing": true, - // "parametric_contracts":["EtherFiNode"], "build_cache": true, "loop_iter": "3", "solc": "solc8.24", "msg": "EtherFiNode", - "rule": ["registerValidatorThenUnregisteringNeverReverts", "associatedValidatorIdsLengthEqNumOfValidators"], } diff --git a/certora/specs/EtherFiNode.spec b/certora/specs/EtherFiNode.spec index 489d8654..0a8f860f 100644 --- a/certora/specs/EtherFiNode.spec +++ b/certora/specs/EtherFiNode.spec @@ -1,50 +1,9 @@ import "./EtherFiNodeSetup.spec"; -use invariant mirrorLength; -use invariant validatorPastLengthAreNullified; -use invariant validatorIndeciesLessThanLength; -use invariant validatorIndeciesValidaorIdMirror; -use invariant blockNumberValidity; use invariant validatorIdsAreUnique; use invariant validatorIdNeverZero; -use builtin rule sanity; - -rule integrityRegisterValidator(uint256 validatorId, bool enableRestaking) { - env e; - requireInvariant validatorIndeciesValidaorIdMirror(); - require version() == 1; - require validatorId != 0; - - mathint numOfValidatorsPre = sumAllAssociatedValidatorIds; - require numOfValidatorsPre < max_uint256; - - bool validatorExistsPre = (associatedValidatorIndicesGhost[validatorId] != 0); - - registerValidator(e, validatorId, enableRestaking); - - bool validatorExistsPost = (associatedValidatorIndicesGhost[validatorId] != 0); - - mathint numOfValidatorsPost = sumAllAssociatedValidatorIds; - - assert !validatorExistsPre && validatorExistsPost => numOfValidatorsPost == numOfValidatorsPre + 1; - assert !validatorExistsPre => associatedValidatorIdsGhost[assert_uint256(numOfValidatorsPre)] == validatorId; - assert !validatorExistsPre => associatedValidatorIndicesGhost[validatorId] == numOfValidatorsPre; -} - -rule integrityOfUnregisterValidator(uint256 validatorId, IEtherFiNodesManager.ValidatorInfo info) { - env e; - bool succeed; - - mathint numOfValidatorsPre = sumAllAssociatedValidatorIds; - - bool validatorExistsPre = (associatedValidatorIndicesGhost[validatorId] != 0); - - succeed = unRegisterValidator(e, validatorId, info); - - bool validatorExistsPost = (associatedValidatorIndicesGhost[validatorId] != 0); - assert false; -} +/// @title whenever the pending withdrawal amount is decreased (completed) the number of completed withdrawals increases. rule pendingComplitedWithdrawalsCorrelation(method f) { env e; calldataarg args; @@ -60,18 +19,7 @@ rule pendingComplitedWithdrawalsCorrelation(method f) { assert pendingPost < pendingPre => completedPost > completedPre; } -rule whoLeaveEth(method f, address membershipAddress) { - env e; - // require membershipAddress != e.msg.sender; - // require auctionManager.membershipManagerContractAddress() == membershipAddress; - calldataarg args; - uint256 contractBalancePre = nativeBalances[currentContract]; - f(e,args); - uint256 contractBalancePost = nativeBalances[currentContract]; - assert contractBalancePre == contractBalancePost; -} - -// Verify state diafram from documentation. +/// @title Verify validator state transition diagram from documentation. // State Transition Diagram for StateMachine contract: // // NOT_INITIALIZED <- @@ -106,14 +54,7 @@ rule validatorStateTransitions(IEtherFiNode.VALIDATOR_PHASE oldPhase, IEtherFiNo assert phaseAfter == WAITING_FOR_APPROVAL() => phaseBefore == STAKE_DEPOSITED(), "WAITING_FOR_APPROVAL transtion violated"; } -// version is always 1 (after initialization). -invariant versionIsOne() - version() == 1; - -invariant sumAllExitedLessThanAllAssociated() - assert_uint256(numExitedValidators() + numExitRequestsByTnft()) <= numAssociatedValidators(); - -//TODO: if NOT_INITIALIZED how can be associated???? +/// @title registering a validator and then unregistering it should never revert. rule registerValidatorThenUnregisteringNeverReverts(uint256 validatorId, bool enableRestaking) { env e; IEtherFiNodesManager.ValidatorInfo info; @@ -123,13 +64,13 @@ rule registerValidatorThenUnregisteringNeverReverts(uint256 validatorId, bool en registerValidator(e, validatorId, enableRestaking); // set validator phase to IEtherFiNode.VALIDATOR_PHASE.STAKE_DEPOSITED - required by the node manager. - require info.validatorIndex == 0; // requires by the node manager. + require info.validatorIndex == 0; require (info.phase == NOT_INITIALIZED() || info.phase == FULLY_WITHDRAWN()); // requires by the node manager. if (info.phase == FULLY_WITHDRAWN()) { require numExitedValidators() > 0; // FULLY_WITHDRAWN can be only if exited before. } - require info.exitRequestTimestamp == 0; // seens to be a deprecated filed in the struct. + require info.exitRequestTimestamp == 0; // seems to be a deprecated filed in the struct. bool succeed = unRegisterValidator@withrevert(e, validatorId, info); @@ -138,17 +79,19 @@ rule registerValidatorThenUnregisteringNeverReverts(uint256 validatorId, bool en assert !didRevert; } +// This invariant is artificially true for the sake of registerValidatorThenUnregisteringNeverReverts. +// it is not accurate because associatedValidatorIdsLengthGhost counts validators in STAKE_DEPOSITED, WAITING_FOR_APPROVAL phases as well. invariant associatedValidatorIdsLengthEqNumOfValidators() associatedValidatorIdsLengthGhost == numAssociatedValidators() + filtered { f -> f.selector != sig:updateNumberOfAssociatedValidators(uint16,uint16).selector } { preserved { - requireInvariant versionIsOne(); + require version() == 1; } preserved unRegisterValidator(uint256 validatorId, IEtherFiNodesManager.ValidatorInfo info) with (env e) { if (info.phase == FULLY_WITHDRAWN() && numAssociatedValidators() > 0) { - // TODO: is it even possible with the tool? updateNumberOfAssociatedValidators(e, 0, 1); // done by node manager at fullWithdraw. (calls processFullWithdraw). - // associatedValidatorIdsLengthGhost = assert_uint256(associatedValidatorIdsLengthGhost - 1); // was never in this array if NOT_INITIALIZED. } else if (info.phase == NOT_INITIALIZED() && associatedValidatorIdsLengthGhost > 0) { + // phase is NOT_INITIALIZED so shouldn't be in numAssociatedValidators. updateNumberOfAssociatedValidators(e, 0, 1); // done by node manager at fullWithdraw. (calls processFullWithdraw). } } @@ -157,18 +100,8 @@ invariant associatedValidatorIdsLengthEqNumOfValidators() associatedValidatorIdsLengthGhost = assert_uint256(associatedValidatorIdsLengthGhost - 1); // done by node manager at fullWithdraw. (calls unregister before) } } + preserved registerValidator(uint256 validatorId, bool restakingEnabled) with (env e) { + // phase is STAKE_DEPOSITED so shouldn't be in numAssociatedValidators. + updateNumberOfAssociatedValidators(e, 1, 0); // should fail for register validator. this is a patch. + } } - -// numexited + num exited < numallassosiated - -// pending Gwei correlation with assosiatedValidators -// invariant pendingGweiAssociatedValidatorsCorrelation() - -// restakingObservedExitBlocks are less than current.block - only for corrcness (may cause false violations) - -// for node manager: -// no same validatorId is present/assosiated in defferent etherFiNodes -// sumAllAssociatedValidatorIds equals _numAssociatedValidators - because it is update in the manager while sumAllAssociatedValidatorIds is tracked through the node itself -// sumAllAssociatedValidatorIds equals sum of validators in a suitable PHASE. -// _numAssociatedValidators equals sum of validators in a suitable PHASE. - diff --git a/certora/specs/EtherFiNodeSetup.spec b/certora/specs/EtherFiNodeSetup.spec index 81bfa85e..107561d2 100644 --- a/certora/specs/EtherFiNodeSetup.spec +++ b/certora/specs/EtherFiNodeSetup.spec @@ -1,30 +1,29 @@ +using EtherFiNode as etherFiNode; + methods { // Getters: - function eigenPod() external returns (address) envfree; - function isRestakingEnabled() external returns (bool) envfree; - function version() external returns (uint16) envfree; - function _numAssociatedValidators() internal returns (uint16); - function associatedValidatorIndices(uint256) external returns (uint256) envfree; - function numExitedValidators() external returns (uint16) envfree; - function numExitRequestsByTnft() external returns (uint16) envfree; - function associatedValidatorIds(uint256) external returns (uint256) envfree; + function etherFiNode.version() external returns (uint16) envfree; + function etherFiNode._numAssociatedValidators() internal returns (uint16); + function etherFiNode.associatedValidatorIndices(uint256) external returns (uint256) envfree; + function etherFiNode.numExitedValidators() external returns (uint16) envfree; + function etherFiNode.numExitRequestsByTnft() external returns (uint16) envfree; + function etherFiNode.associatedValidatorIds(uint256) external returns (uint256) envfree; // Track the amount of pending/completed withdrawals; - function pendingWithdrawalFromRestakingInGwei() external returns (uint64) envfree; - function completedWithdrawalFromRestakingInGwei() external returns (uint64) envfree; - function updateNumberOfAssociatedValidators(uint16, uint16) external; + function etherFiNode.pendingWithdrawalFromRestakingInGwei() external returns (uint64) envfree; + function etherFiNode.completedWithdrawalFromRestakingInGwei() external returns (uint64) envfree; + function etherFiNode.updateNumberOfAssociatedValidators(uint16, uint16) external; - function numAssociatedValidators() external returns (uint256) envfree; - function registerValidator(uint256, bool) external; - function validatePhaseTransition(IEtherFiNode.VALIDATOR_PHASE, IEtherFiNode.VALIDATOR_PHASE) external returns (bool) envfree; + function etherFiNode.numAssociatedValidators() external returns (uint256) envfree; + function etherFiNode.registerValidator(uint256, bool) external; + function etherFiNode.validatePhaseTransition(IEtherFiNode.VALIDATOR_PHASE, IEtherFiNode.VALIDATOR_PHASE) external returns (bool) envfree; // IEigenPodManager summaries: function _.eigenPodManager() external => NONDET; function _.getPod(address) external => NONDET; function _.createPod() external => NONDET; - // munge: - function getAssociatedValidatorIdsLength() external returns (uint256) envfree; - + // IEigenPod summaries: + function _.withdrawableRestakedExecutionLayerGwei() external => NONDET; } definition NOT_INITIALIZED() returns IEtherFiNode.VALIDATOR_PHASE = IEtherFiNode.VALIDATOR_PHASE.NOT_INITIALIZED; @@ -35,22 +34,17 @@ definition FULLY_WITHDRAWN() returns IEtherFiNode.VALIDATOR_PHASE = IEtherFiNode definition BEING_SLASHED() returns IEtherFiNode.VALIDATOR_PHASE = IEtherFiNode.VALIDATOR_PHASE.BEING_SLASHED; definition WAITING_FOR_APPROVAL() returns IEtherFiNode.VALIDATOR_PHASE = IEtherFiNode.VALIDATOR_PHASE.WAITING_FOR_APPROVAL; -// CALL FORWARDING filtered: -definition callForwarding(method f) returns bool = - f.selector == sig:callEigenPod(bytes).selector || - f.selector == sig:forwardCall(address, bytes).selector; - persistent ghost uint256 associatedValidatorIdsLengthGhost { init_state axiom associatedValidatorIdsLengthGhost == 0; + axiom associatedValidatorIdsLengthGhost < max_uint128; } -persistent ghost mapping(uint256 => uint256) associatedValidatorIndicesGhost { - init_state axiom forall uint256 validator . associatedValidatorIndicesGhost[validator] == 0; +ghost uint256 biggestValidatorIndex { + init_state axiom biggestValidatorIndex == 0; } -persistent ghost mathint sumAllAssociatedValidatorIndicesGhost { - init_state axiom sumAllAssociatedValidatorIndicesGhost == 0; - axiom sumAllAssociatedValidatorIndicesGhost >= 0; +persistent ghost mapping(uint256 => uint256) associatedValidatorIndicesGhost { + init_state axiom forall uint256 validator . associatedValidatorIndicesGhost[validator] == 0; } persistent ghost mapping(uint256 => uint256) associatedValidatorIdsGhost { @@ -69,88 +63,66 @@ persistent ghost mapping(uint256 => uint32) restakingObservedExitBlocksGhost { init_state axiom forall uint256 validatorId . restakingObservedExitBlocksGhost[validatorId] == 0; } -hook Sstore restakingObservedExitBlocks[KEY uint256 validatorId] uint32 newblock (uint32 oldBlock) { +hook Sstore etherFiNode.restakingObservedExitBlocks[KEY uint256 validatorId] uint32 newblock (uint32 oldBlock) { if (newblock > latestBlockGhost) { latestBlockGhost = newblock; } restakingObservedExitBlocksGhost[validatorId] = newblock; } -hook Sload uint32 blockNumber restakingObservedExitBlocks[KEY uint256 validatorId] { +hook Sload uint32 blockNumber etherFiNode.restakingObservedExitBlocks[KEY uint256 validatorId] { require blockNumber == restakingObservedExitBlocksGhost[validatorId]; } -hook Sstore associatedValidatorIds.(offset 0) uint256 newlength (uint256 oldlength) { +hook Sstore etherFiNode.associatedValidatorIds.(offset 0) uint256 newlength (uint256 oldlength) { require oldlength == associatedValidatorIdsLengthGhost; associatedValidatorIdsLengthGhost = newlength; } -hook Sload uint256 length associatedValidatorIds.(offset 0) { +hook Sload uint256 length etherFiNode.associatedValidatorIds.(offset 0) { require length == associatedValidatorIdsLengthGhost; } -hook Sstore associatedValidatorIndices[KEY uint256 validator] uint256 newIndecies (uint256 oldIndecies) { +hook Sstore etherFiNode.associatedValidatorIndices[KEY uint256 validator] uint256 newIndecies (uint256 oldIndecies) { + require oldIndecies == associatedValidatorIndicesGhost[validator]; + if (newIndecies > biggestValidatorIndex) { biggestValidatorIndex = newIndecies; } associatedValidatorIndicesGhost[validator] = newIndecies; - sumAllAssociatedValidatorIndicesGhost = sumAllAssociatedValidatorIndicesGhost + newIndecies - oldIndecies; } -hook Sload uint256 indecies associatedValidatorIndices[KEY uint256 validator] { +hook Sload uint256 indecies etherFiNode.associatedValidatorIndices[KEY uint256 validator] { require indecies == associatedValidatorIndicesGhost[validator]; } -hook Sstore associatedValidatorIds[INDEX uint256 index] uint256 newValidator (uint256 oldValidator) { - if (newValidator == 0 && oldValidator != 0) { +hook Sstore etherFiNode.associatedValidatorIds[INDEX uint256 index] uint256 newValidator (uint256 oldValidator) { + require oldValidator == associatedValidatorIdsGhost[index]; + if (newValidator == 0 && oldValidator != 0) { // removing a validator sumAllAssociatedValidatorIds = sumAllAssociatedValidatorIds - 1; - } else if (newValidator != 0 && oldValidator == 0) { + } else if (newValidator != 0 && oldValidator == 0) { // adding new validator sumAllAssociatedValidatorIds = sumAllAssociatedValidatorIds + 1; } associatedValidatorIdsGhost[index] = newValidator; } -hook Sload uint256 validator associatedValidatorIds[INDEX uint256 index] { +hook Sload uint256 validator etherFiNode.associatedValidatorIds[INDEX uint256 index] { require validator == associatedValidatorIdsGhost[index]; } -invariant mirrorLength() - associatedValidatorIdsLengthGhost == getAssociatedValidatorIdsLength(); - -invariant validatorIndeciesLessThanLength(uint256 validatorId, uint256 index) - forall uint256 validator . associatedValidatorIndicesGhost[validator] <= associatedValidatorIdsLengthGhost; - -invariant validatorPastLengthAreNullified() - forall uint256 index . index > associatedValidatorIdsLengthGhost => associatedValidatorIdsGhost[index] == 0 - { - preserved registerValidator(uint256 validatorId, bool redtskingEnabled) with (env e) { - require validatorId != 0; - } - } - -// invariant mirrorIntegrity(uint256 index) -// index < associatedValidatorIdsLengthGhost => -// associatedValidatorIndicesGhost[associatedValidatorIdsGhost[index]] == index && -// associatedValidatorIdsGhost[associatedValidatorIndicesGhost[validator]] == validator; - -invariant validatorIndeciesValidaorIdMirror() - forall uint256 validatorId . associatedValidatorIndicesGhost[validatorId] != 0 => - associatedValidatorIdsGhost[associatedValidatorIndicesGhost[validatorId]] == validatorId; +function validatorNotInArray(uint256 validatorId) returns bool { + return forall uint256 indx . indx < associatedValidatorIdsLengthGhost => + associatedValidatorIdsGhost[indx] != validatorId; +} +/// @title Verifies that any associated validator ID can never be zero. invariant validatorIdNeverZero() forall uint256 index . index < associatedValidatorIdsLengthGhost => associatedValidatorIdsGhost[index] != 0 { - preserved registerValidator(uint256 validatorId, bool redtskingEnabled) with (env e) { + preserved etherFiNode.registerValidator(uint256 validatorId, bool redtskingEnabled) with (env e) { // validatorId starts from 1. require validatorId != 0; } } -// invariant validatorIndeciesValidaorIdMirror() -// forall uint256 validatorId . associatedValidatorIndices(validatorId) != 0 => -// associatedValidatorIds(associatedValidatorIndices(validatorId)) == validatorId; - -// it is not proven and might be allowed by the system but it helps to prove properties on the EtherFiNode. -// invariant validatorIdsAreUnique(uint256 validatorId) if there are two different indexes then their validatorId is different (if indexes less than length) -// (validatorId != 0 && associatedValidatorIndicesGhost[validatorId] == 0) => (forall uint256 index . associatedValidatorIdsGhost[index] != validatorId); - +// for use in future rules - requires that the current block number is valid. invariant blockNumberValidity(uint32 blockNumber) blockNumber >= latestBlockGhost { @@ -159,6 +131,7 @@ invariant blockNumberValidity(uint32 blockNumber) } } +/// @title Verifies that the associated validator IDs are unique. invariant validatorIdsAreUnique() forall uint256 index1 . forall uint256 index2 . (index1 != index2 && index1 < associatedValidatorIdsLengthGhost && index2 < associatedValidatorIdsLengthGhost) => @@ -166,9 +139,16 @@ invariant validatorIdsAreUnique() { preserved with (env e) { requireInvariant validatorIdNeverZero(); - requireInvariant validatorPastLengthAreNullified(); + // proven in versionIsOneOnlyIfAssociated() invariant. + require associatedValidatorIdsLengthGhost > 0 => etherFiNode.version == 1; } + preserved etherFiNode.registerValidator(uint256 validatorId, bool redtskingEnabled) with (env e) { + // validatorId starts from 1. + require validatorId != 0; + // EtherFiNodeManager requires that the validator is not already installed in this node - + // the invariant amountOfValidatorPerEtherFiNodeEqualsNumAssociatedValidators() combined with this followinh code ensures that it is safe: + // (etherfiNodeAddress[_validatorId] != address(0)) revert AlreadyInstalled(); + require validatorNotInArray(validatorId); + } } - - - // אם אינדקס קטן אז שונה מאפס ואם גדול אז שווה לאפס + \ No newline at end of file From b0f8ccdc8e74846026bd5c61101dc5d3793b2bc8 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Wed, 18 Sep 2024 17:45:20 +0300 Subject: [PATCH 23/26] add etherfi nodes manager specs --- certora/config/EtherFiNodesManager.conf | 27 +++ certora/specs/EtherFiNodesManagerSetup.spec | 222 ++++++++++++++++++++ 2 files changed, 249 insertions(+) create mode 100644 certora/config/EtherFiNodesManager.conf create mode 100644 certora/specs/EtherFiNodesManagerSetup.spec diff --git a/certora/config/EtherFiNodesManager.conf b/certora/config/EtherFiNodesManager.conf new file mode 100644 index 00000000..8cdaeea4 --- /dev/null +++ b/certora/config/EtherFiNodesManager.conf @@ -0,0 +1,27 @@ +{ + "files": [ + "src/EtherFiNodesManager.sol", + "src/EtherFiNode.sol", + "src/TNFT.sol", + "src/BNFT.sol", + "src/RoleRegistry.sol", + ], + "link": [ + "EtherFiNodesManager:tnft=TNFT", + "EtherFiNodesManager:bnft=BNFT", + "EtherFiNodesManager:roleRegistry=RoleRegistry", + ], + "packages": [ + "@openzeppelin=lib/openzeppelin-contracts", + "forge-std=lib/forge-std/src" + ], + "verify": "EtherFiNodesManager:certora/specs/EtherFiNodesManagerSetup.spec", + "optimistic_loop": true, + "optimistic_fallback": true, + "optimistic_hashing": true, + "parametric_contracts":["EtherFiNodesManager"], + "build_cache": true, + "loop_iter": "3", + "solc": "solc8.24", + "msg": "EtherFiNodesManager all rules", +} diff --git a/certora/specs/EtherFiNodesManagerSetup.spec b/certora/specs/EtherFiNodesManagerSetup.spec new file mode 100644 index 00000000..47e3061c --- /dev/null +++ b/certora/specs/EtherFiNodesManagerSetup.spec @@ -0,0 +1,222 @@ +import "./EtherFiNodeSetup.spec"; +import "./nftDispach.spec"; +import "./EtherFiNodeInterface.spec"; + +using EtherFiNodesManager as etherFiNodesManager; + +methods { + // Getters: + function numberOfValidators() external returns (uint64) envfree; // # of validators in LIVE or WAITING_FOR_APPROVAL phases + function nonExitPenaltyPrincipal() external returns (uint64) envfree; + function nonExitPenaltyDailyRate() external returns (uint64) envfree; + function SCALE() external returns (uint64) envfree; + function treasuryContract() external returns (address) envfree; + function stakingManagerContract() external returns (address) envfree; + function auctionManager() external returns (address) envfree; + function eigenPodManager() external returns (address) envfree; + function etherfiNodeAddress(uint256) external returns (address) envfree; // validatorId == bidId -> withdrawalSafeAddress + function unusedWithdrawalSafes(uint256) external returns (address) envfree; + + function _.instantiateEtherFiNode(bool) external => createNewNodeAddress() expect (address); + + // delegationManager summaries: + function _.delegationManager() external => NONDET; + function _.beaconChainETHStrategy() external => NONDET; + function _.queueWithdrawals(IDelegationManager.QueuedWithdrawalParams[]) external => NONDET; + function _.completeQueuedWithdrawals(IDelegationManager.Withdrawal[],address[][],uint256[],bool[]) external => NONDET; // external call only. + + // Auction manager summaries: + function _.getBidOwner(uint256) external => NONDET; + + // Deprecated and penalty functions: + function _.DEPRECATED_delayedWithdrawalRouter() external => NONDET; + function _.nonExitPenaltyPrincipal() external => NONDET; + function _.nonExitPenaltyDailyRate() external => NONDET; + + function _.getClaimableUserDelayedWithdrawals(address) external => NONDET; +} + +// Functions filtered out since they forwarding external calls. +definition isFilteredFunc(method f) returns bool = ( + f.selector == sig:forwardEigenpodCall(uint256[],bytes[]).selector || + f.selector == sig:forwardExternalCall(uint256[],bytes[],address).selector || + f.selector == sig:upgradeToAndCall(address, bytes).selector +); + +function nodeNotInArray(address EtherFiNode) returns bool { + return forall uint256 indx . indx < unusedWithdrawalSafesLengthGhost => + unusedWithdrawalSafesMirror[indx] != EtherFiNode; +} + +function nodeNotInAddresses(address EtherFiNode) returns bool { + return forall uint256 validatorId . etherfiNodeAddressMirror[validatorId] != EtherFiNode; +} + +// creates new node address. +function createNewNodeAddress() returns address { + address newAddress; + require nodeNotInArray(newAddress); + require nodeNotInAddresses(newAddress); + require newAddress != 0; + return newAddress; +} + +ghost mapping(uint256 => address) etherfiNodeAddressMirror { + init_state axiom forall uint256 validatorId . etherfiNodeAddressMirror[validatorId] == 0; +} + +ghost uint256 unusedWithdrawalSafesLengthGhost { + init_state axiom unusedWithdrawalSafesLengthGhost == 0; +} + +ghost mapping(uint256 => address) unusedWithdrawalSafesMirror { + init_state axiom forall uint256 index . unusedWithdrawalSafesMirror[index] == 0; +} + +ghost mapping(address => mathint) associatedValidatorsPerNode { + init_state axiom forall address node . associatedValidatorsPerNode[node] == 0; +} + +hook Sstore etherFiNodesManager.unusedWithdrawalSafes[INDEX uint256 indx] address newSafe (address oldSafe) { + require oldSafe == unusedWithdrawalSafesMirror[indx]; + unusedWithdrawalSafesMirror[indx] = newSafe; +} + +hook Sload address safe etherFiNodesManager.unusedWithdrawalSafes[INDEX uint256 indx] { + require safe == unusedWithdrawalSafesMirror[indx]; +} + +hook Sstore etherFiNodesManager.etherfiNodeAddress[KEY uint256 validatorId] address newNode (address oldNode) { + require oldNode == etherfiNodeAddressMirror[validatorId]; + if (oldNode == 0 && newNode != 0) { + associatedValidatorsPerNode[newNode] = associatedValidatorsPerNode[newNode] + 1; + } else if (oldNode != 0 && newNode == 0) { + associatedValidatorsPerNode[oldNode] = associatedValidatorsPerNode[oldNode] - 1; + } + etherfiNodeAddressMirror[validatorId] = newNode; +} + +hook Sload address node etherFiNodesManager.etherfiNodeAddress[KEY uint256 validatorId] { + require node == etherfiNodeAddressMirror[validatorId]; +} + +// hook unusedWithdrawalSafes length +hook Sstore etherFiNodesManager.unusedWithdrawalSafes.(offset 0) uint256 newlength (uint256 oldlength) { + require oldlength == unusedWithdrawalSafesLengthGhost; + unusedWithdrawalSafesLengthGhost = newlength; + // POP(): + if (oldlength - newlength == 1) { + unusedWithdrawalSafesMirror[newlength] = 0; + } +} + +hook Sload uint256 length etherFiNodesManager.unusedWithdrawalSafes.(offset 0) { + require length == unusedWithdrawalSafesLengthGhost; +} + +/// @title Verifies that mirroring unusedWithdrawalSafesMirror is done correctly. +invariant ArrayMirrorIntegrity() + forall uint256 indx. + (indx < unusedWithdrawalSafesLengthGhost => unusedWithdrawalSafesMirror[indx] != 0) && + (indx >= unusedWithdrawalSafesLengthGhost && indx < max_uint256 => unusedWithdrawalSafesMirror[indx] == 0) + filtered {f -> !isFilteredFunc(f)} + { + preserved { + require unusedWithdrawalSafesLengthGhost < max_uint256 - 3; // -3 for every possible loop iteration. + } + } + +/// @title Verifies that the amout of linked validators to a node by the manager equals the actual amount of associated validators by the node itseld. +invariant amountOfValidatorPerEtherFiNodeEqualsNumAssociatedValidators() + associatedValidatorIdsLengthGhost == associatedValidatorsPerNode[etherFiNode] + filtered {f -> !isFilteredFunc(f)} + { + preserved { + require etherFiNode.version() == 1; + } + } + +ghost mathint minimalLength; +ghost bool atLeastOnAssociated; + +function noValidatorForUnusedNodesRequirements(uint256 validatorId) { + requireInvariant ArrayMirrorIntegrity(); + // push node to unused safes only if it is the last associated validator: + requireInvariant amountOfValidatorPerEtherFiNodeEqualsNumAssociatedValidators(); + // require etherFiNode.version() == 1; + requireInvariant versionIsOneOnlyIfAssociated(); + requireInvariant validatorIdNeverZero(); + requireInvariant noValidatorForUnusedNodes(validatorId); + require unusedWithdrawalSafesLengthGhost < max_uint256 - 3; // -3 for every possible loop iteration. +} + +/// @title Verifies that if there is a node in unused nodes array than there is no validator that is linked to it. +invariant noValidatorForUnusedNodes(uint256 validatorId) + forall uint256 indx . indx < unusedWithdrawalSafesLengthGhost && validatorId != 0 => + unusedWithdrawalSafesMirror[indx] != etherfiNodeAddressMirror[validatorId] + filtered {f -> !isFilteredFunc(f)} + { + preserved { + requireInvariant ArrayMirrorIntegrity(); + } + preserved registerValidator(uint256 _validatorId, bool _enableRestaking, address _withdrawalSafeAddress) with (env e) { + // staking manager call allocate etherfi node before this call. which means it is safe to assume _withdrawalSafeAddress is not in unusedSafes. + require nodeNotInArray(_withdrawalSafeAddress); + requireInvariant ArrayMirrorIntegrity(); + } + preserved unregisterValidator(uint256 _validatorId) with (env e) { + noValidatorForUnusedNodesRequirements(_validatorId); + require (etherfiNodeAddress(_validatorId) == etherfiNodeAddress(validatorId)) => associatedValidatorIdsLengthGhost >= 2; + } + preserved fullWithdraw(uint256 _validatorId) with (env e) { + noValidatorForUnusedNodesRequirements(_validatorId); + require (etherfiNodeAddress(_validatorId) == etherfiNodeAddress(validatorId)) => associatedValidatorIdsLengthGhost >= 2; + } + preserved batchFullWithdraw(uint256[] _validatorIds) with (env e) { + noValidatorForUnusedNodesRequirements(_validatorIds[0]); + requireInvariant noValidatorForUnusedNodes(_validatorIds[1]); + requireInvariant noValidatorForUnusedNodes(_validatorIds[2]); + minimalLength = 0; + atLeastOnAssociated = false; // Using this for not excluding zero length case. + if (etherfiNodeAddress(_validatorIds[0]) == etherfiNodeAddress(validatorId)) { minimalLength = minimalLength + 1; atLeastOnAssociated = true;} + if (etherfiNodeAddress(_validatorIds[1]) == etherfiNodeAddress(validatorId)) { minimalLength = minimalLength + 1; atLeastOnAssociated = true;} + if (etherfiNodeAddress(_validatorIds[2]) == etherfiNodeAddress(validatorId)) { minimalLength = minimalLength + 1; atLeastOnAssociated = true;} + if (etherfiNodeAddress(_validatorIds[0]) == etherfiNodeAddress(_validatorIds[1])) { minimalLength = minimalLength + 1; atLeastOnAssociated = true;} + if (etherfiNodeAddress(_validatorIds[0]) == etherfiNodeAddress(_validatorIds[2])) { minimalLength = minimalLength + 1; atLeastOnAssociated = true;} + if (etherfiNodeAddress(_validatorIds[1]) == etherfiNodeAddress(_validatorIds[2])) { minimalLength = minimalLength + 1; atLeastOnAssociated = true;} + if (atLeastOnAssociated) { minimalLength = minimalLength + 1;} + require associatedValidatorIdsLengthGhost >= minimalLength; + } + } + +invariant unusedWithdrawalSafesUniqueness(uint256 indx1, uint256 indx2) + indx1 != indx2 && indx1 < unusedWithdrawalSafesLengthGhost && indx2 < unusedWithdrawalSafesLengthGhost => + unusedWithdrawalSafesMirror[indx1] != unusedWithdrawalSafesMirror[indx2] + filtered {f -> !isFilteredFunc(f)} + { + preserved { + require unusedWithdrawalSafesLengthGhost < max_uint256 - 3; // -3 for every possible loop iteration. + } + preserved unregisterValidator(uint256 _validatorId) with (env e) { + require _validatorId != 0; + requireInvariant noValidatorForUnusedNodes(_validatorId); + } + preserved fullWithdraw(uint256 _validatorId) with (env e) { + require _validatorId != 0; + requireInvariant noValidatorForUnusedNodes(_validatorId); + } + preserved batchFullWithdraw(uint256[] _validatorIds) with (env e) { + require _validatorIds[0] != 0; + require _validatorIds[1] != 0; + require _validatorIds[2] != 0; + requireInvariant noValidatorForUnusedNodes(_validatorIds[0]); + requireInvariant noValidatorForUnusedNodes(_validatorIds[1]); + requireInvariant noValidatorForUnusedNodes(_validatorIds[2]); + } + } + +/// @title Verifies that if there are associated validators to a node then its version is one. +invariant versionIsOneOnlyIfAssociated() + associatedValidatorsPerNode[etherFiNode] > 0 => etherFiNode.version == 1 + filtered {f -> !isFilteredFunc(f)} + \ No newline at end of file From df1b9bb09c3c8cdeb91f091ad014e3a69d706b63 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Thu, 19 Sep 2024 10:21:01 +0300 Subject: [PATCH 24/26] remove redundant --- certora/specs/EtherFiNodesManagerSetup.spec | 1 - 1 file changed, 1 deletion(-) diff --git a/certora/specs/EtherFiNodesManagerSetup.spec b/certora/specs/EtherFiNodesManagerSetup.spec index 47e3061c..8f6c9e9f 100644 --- a/certora/specs/EtherFiNodesManagerSetup.spec +++ b/certora/specs/EtherFiNodesManagerSetup.spec @@ -143,7 +143,6 @@ function noValidatorForUnusedNodesRequirements(uint256 validatorId) { requireInvariant ArrayMirrorIntegrity(); // push node to unused safes only if it is the last associated validator: requireInvariant amountOfValidatorPerEtherFiNodeEqualsNumAssociatedValidators(); - // require etherFiNode.version() == 1; requireInvariant versionIsOneOnlyIfAssociated(); requireInvariant validatorIdNeverZero(); requireInvariant noValidatorForUnusedNodes(validatorId); From 5ab7b00aee5bcd8ad9645490eb2dcd462a6b6b5b Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Thu, 19 Sep 2024 18:01:54 +0300 Subject: [PATCH 25/26] update comments and documentation --- certora/specs/EtherFiNode.spec | 2 +- certora/specs/EtherFiNodesManagerSetup.spec | 55 +++++++++++++++++---- 2 files changed, 47 insertions(+), 10 deletions(-) diff --git a/certora/specs/EtherFiNode.spec b/certora/specs/EtherFiNode.spec index 0a8f860f..0ae0743a 100644 --- a/certora/specs/EtherFiNode.spec +++ b/certora/specs/EtherFiNode.spec @@ -42,7 +42,7 @@ rule validatorStateTransitions(IEtherFiNode.VALIDATOR_PHASE oldPhase, IEtherFiNo bool res; IEtherFiNode.VALIDATOR_PHASE phaseBefore = oldPhase; - res = validatePhaseTransition(oldPhase, newPhase); // call phase instead. + res = validatePhaseTransition(oldPhase, newPhase); IEtherFiNode.VALIDATOR_PHASE phaseAfter = newPhase; assert phaseAfter == NOT_INITIALIZED() => phaseBefore == NOT_INITIALIZED() || phaseBefore == STAKE_DEPOSITED() || phaseBefore == WAITING_FOR_APPROVAL(), "NOT_INITIALIZED transtion violated"; diff --git a/certora/specs/EtherFiNodesManagerSetup.spec b/certora/specs/EtherFiNodesManagerSetup.spec index 8f6c9e9f..5158040a 100644 --- a/certora/specs/EtherFiNodesManagerSetup.spec +++ b/certora/specs/EtherFiNodesManagerSetup.spec @@ -61,22 +61,39 @@ function createNewNodeAddress() returns address { return newAddress; } +/****** Ghost declaration *****/ + +/** @title Ghost etherfiNodeAddressMirror is: + mirrors the etherfiNodeAddress map for further use with quantifiers. +**/ ghost mapping(uint256 => address) etherfiNodeAddressMirror { + // assuming value zero at the initial state before constructor init_state axiom forall uint256 validatorId . etherfiNodeAddressMirror[validatorId] == 0; } +/** Ghost unusedWithdrawalSafesLengthGhost is: + mirrors the unusedWithdrawalSafes length. +**/ ghost uint256 unusedWithdrawalSafesLengthGhost { init_state axiom unusedWithdrawalSafesLengthGhost == 0; } +/** Ghost unusedWithdrawalSafesMirror is: + mirrors the unusedWithdrawalSafes arrray for further use with quantifiers. +**/ ghost mapping(uint256 => address) unusedWithdrawalSafesMirror { init_state axiom forall uint256 index . unusedWithdrawalSafesMirror[index] == 0; } +/** Ghost associatedValidatorsPerNode is: + count the number of validator pointing to the same etherFi node at etherfiNodeAddress. +**/ ghost mapping(address => mathint) associatedValidatorsPerNode { init_state axiom forall address node . associatedValidatorsPerNode[node] == 0; } +/****** Hooks for ghost updates *****/ + hook Sstore etherFiNodesManager.unusedWithdrawalSafes[INDEX uint256 indx] address newSafe (address oldSafe) { require oldSafe == unusedWithdrawalSafesMirror[indx]; unusedWithdrawalSafesMirror[indx] = newSafe; @@ -100,7 +117,7 @@ hook Sload address node etherFiNodesManager.etherfiNodeAddress[KEY uint256 valid require node == etherfiNodeAddressMirror[validatorId]; } -// hook unusedWithdrawalSafes length +// updates unusedWithdrawalSafes length hook Sstore etherFiNodesManager.unusedWithdrawalSafes.(offset 0) uint256 newlength (uint256 oldlength) { require oldlength == unusedWithdrawalSafesLengthGhost; unusedWithdrawalSafesLengthGhost = newlength; @@ -114,7 +131,7 @@ hook Sload uint256 length etherFiNodesManager.unusedWithdrawalSafes.(offset 0) { require length == unusedWithdrawalSafesLengthGhost; } -/// @title Verifies that mirroring unusedWithdrawalSafesMirror is done correctly. +/** @title Verifies that mirroring unusedWithdrawalSafesMirror is done correctly. **/ invariant ArrayMirrorIntegrity() forall uint256 indx. (indx < unusedWithdrawalSafesLengthGhost => unusedWithdrawalSafesMirror[indx] != 0) && @@ -126,7 +143,8 @@ invariant ArrayMirrorIntegrity() } } -/// @title Verifies that the amout of linked validators to a node by the manager equals the actual amount of associated validators by the node itseld. +/** @title Verifies that the amout of linked validators to a node by the manager +equals the actual amount of associated validators by the node itself. **/ invariant amountOfValidatorPerEtherFiNodeEqualsNumAssociatedValidators() associatedValidatorIdsLengthGhost == associatedValidatorsPerNode[etherFiNode] filtered {f -> !isFilteredFunc(f)} @@ -136,17 +154,26 @@ invariant amountOfValidatorPerEtherFiNodeEqualsNumAssociatedValidators() } } +// helper ghosts to count the amount of validatorIds associated with the etherFi node. ghost mathint minimalLength; ghost bool atLeastOnAssociated; -function noValidatorForUnusedNodesRequirements(uint256 validatorId) { - requireInvariant ArrayMirrorIntegrity(); +/** + CVL function to gather all valid state needed for noValidatorForUnusedNodes invariant and one other assumption: + 1. the size of the unusedWithdrawalSafes array is not close to max_uint. +**/ +function validStateForNoValidatorForUnusedNodes(uint256 validatorId) { + requireInvariant ArrayMirrorIntegrity(); // require that the ghost mirroring is correct. // push node to unused safes only if it is the last associated validator: requireInvariant amountOfValidatorPerEtherFiNodeEqualsNumAssociatedValidators(); + /* required to avoid invalid state where node version is zero + and there are validators associated with the node. */ requireInvariant versionIsOneOnlyIfAssociated(); requireInvariant validatorIdNeverZero(); + // require the invariant is correct for the new validatorId as well for the prestate. requireInvariant noValidatorForUnusedNodes(validatorId); - require unusedWithdrawalSafesLengthGhost < max_uint256 - 3; // -3 for every possible loop iteration. + // -1 for every possible loop iteration (loop_iter = 3) to avoid overflows. + require unusedWithdrawalSafesLengthGhost < max_uint256 - 3; } /// @title Verifies that if there is a node in unused nodes array than there is no validator that is linked to it. @@ -164,17 +191,20 @@ invariant noValidatorForUnusedNodes(uint256 validatorId) requireInvariant ArrayMirrorIntegrity(); } preserved unregisterValidator(uint256 _validatorId) with (env e) { - noValidatorForUnusedNodesRequirements(_validatorId); + validStateForNoValidatorForUnusedNodes(_validatorId); + // If there are two validator pointing to the same etherFi node then its associated validatorIds length must be at least 2. require (etherfiNodeAddress(_validatorId) == etherfiNodeAddress(validatorId)) => associatedValidatorIdsLengthGhost >= 2; } preserved fullWithdraw(uint256 _validatorId) with (env e) { - noValidatorForUnusedNodesRequirements(_validatorId); + validStateForNoValidatorForUnusedNodes(_validatorId); + // If there are two validator pointing to the same etherFi node then its associated validatorIds length must be at least 2. require (etherfiNodeAddress(_validatorId) == etherfiNodeAddress(validatorId)) => associatedValidatorIdsLengthGhost >= 2; } preserved batchFullWithdraw(uint256[] _validatorIds) with (env e) { - noValidatorForUnusedNodesRequirements(_validatorIds[0]); + validStateForNoValidatorForUnusedNodes(_validatorIds[0]); requireInvariant noValidatorForUnusedNodes(_validatorIds[1]); requireInvariant noValidatorForUnusedNodes(_validatorIds[2]); + // If there are X amount validator pointing to the same etherFi node then its associated validatorIds length must be at least X. minimalLength = 0; atLeastOnAssociated = false; // Using this for not excluding zero length case. if (etherfiNodeAddress(_validatorIds[0]) == etherfiNodeAddress(validatorId)) { minimalLength = minimalLength + 1; atLeastOnAssociated = true;} @@ -188,6 +218,7 @@ invariant noValidatorForUnusedNodes(uint256 validatorId) } } +/// @title Verifies that there are no duplicated etherFi nodes in the unusedWithdrawalSafes array. invariant unusedWithdrawalSafesUniqueness(uint256 indx1, uint256 indx2) indx1 != indx2 && indx1 < unusedWithdrawalSafesLengthGhost && indx2 < unusedWithdrawalSafesLengthGhost => unusedWithdrawalSafesMirror[indx1] != unusedWithdrawalSafesMirror[indx2] @@ -197,17 +228,23 @@ invariant unusedWithdrawalSafesUniqueness(uint256 indx1, uint256 indx2) require unusedWithdrawalSafesLengthGhost < max_uint256 - 3; // -3 for every possible loop iteration. } preserved unregisterValidator(uint256 _validatorId) with (env e) { + // validatorIds starts from 1. require _validatorId != 0; + // requires that if there is a node in unused nodes array than the following validatorid is not linked to it. requireInvariant noValidatorForUnusedNodes(_validatorId); } preserved fullWithdraw(uint256 _validatorId) with (env e) { + // validatorIds starts from 1. require _validatorId != 0; + // requires that if there is a node in unused nodes array than the following validatorid is not linked to it. requireInvariant noValidatorForUnusedNodes(_validatorId); } preserved batchFullWithdraw(uint256[] _validatorIds) with (env e) { + // validatorIds starts from 1. require _validatorIds[0] != 0; require _validatorIds[1] != 0; require _validatorIds[2] != 0; + // requires that if there is a node in unused nodes array than the following validatorIds are not linked to it. requireInvariant noValidatorForUnusedNodes(_validatorIds[0]); requireInvariant noValidatorForUnusedNodes(_validatorIds[1]); requireInvariant noValidatorForUnusedNodes(_validatorIds[2]); From 705ae29ef6c36ab03c2e9c9a2771765d21e40888 Mon Sep 17 00:00:00 2001 From: Gad Elbaz Date: Thu, 19 Sep 2024 18:12:43 +0300 Subject: [PATCH 26/26] small update --- certora/specs/EtherFiNodesManagerSetup.spec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/certora/specs/EtherFiNodesManagerSetup.spec b/certora/specs/EtherFiNodesManagerSetup.spec index 5158040a..bf421ff7 100644 --- a/certora/specs/EtherFiNodesManagerSetup.spec +++ b/certora/specs/EtherFiNodesManagerSetup.spec @@ -63,7 +63,7 @@ function createNewNodeAddress() returns address { /****** Ghost declaration *****/ -/** @title Ghost etherfiNodeAddressMirror is: +/** Ghost etherfiNodeAddressMirror is: mirrors the etherfiNodeAddress map for further use with quantifiers. **/ ghost mapping(uint256 => address) etherfiNodeAddressMirror {