Skip to content

Commit

Permalink
Update test and summary for unlockStETH
Browse files Browse the repository at this point in the history
  • Loading branch information
@lucasmt
lucasmt committed Aug 6, 2024
1 parent eb7ebd3 commit ad10520
Show file tree
Hide file tree
Showing 2 changed files with 120 additions and 10 deletions.
56 changes: 52 additions & 4 deletions test/kontrol/ActivateNextState.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,11 @@ import "test/kontrol/DualGovernanceSetUp.sol";

contract ActivateNextStateMock is StorageSetup {
StorageSetup public immutable STORAGE_SETUP;
address public immutable USER;

constructor(address storageSetup) {
constructor(address storageSetup, address user) {
STORAGE_SETUP = StorageSetup(storageSetup);
USER = user;
}

function activateNextState() external {
Expand All @@ -22,13 +24,59 @@ contract ActivateNextStateMock is StorageSetup {
STORAGE_SETUP.escrowStorageInvariants(Mode.Assert, rageQuitEscrow);
STORAGE_SETUP.rageQuitEscrowStorageInvariants(Mode.Assert, rageQuitEscrow);

address escrowMasterCopy = signallingEscrow.MASTER_COPY();
IEscrow newSignallingEscrow = IEscrow(Clones.clone(escrowMasterCopy));
IEscrow newRageQuitEscrow = IEscrow(Clones.clone(escrowMasterCopy));
AccountingRecord memory pre = STORAGE_SETUP.saveAccountingRecord(USER, signallingEscrow);

State initialState = dualGovernance.getCurrentState();
uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport();
Timestamp vetoSignallingActivationTime = Timestamp.wrap(_getVetoSignallingActivationTime(dualGovernance));
IConfiguration config = dualGovernance.CONFIG();

IEscrow newSignallingEscrow;
IEscrow newRageQuitEscrow;

bool transitionToRageQuit = (
initialState == State.VetoSignalling || initialState == State.VetoSignallingDeactivation
) && rageQuitSupport > config.SECOND_SEAL_RAGE_QUIT_SUPPORT()
&& Timestamps.now() > config.DYNAMIC_TIMELOCK_MAX_DURATION().addTo(vetoSignallingActivationTime);

if (transitionToRageQuit) {
address escrowMasterCopy = signallingEscrow.MASTER_COPY();
newSignallingEscrow = IEscrow(Clones.clone(escrowMasterCopy));
newRageQuitEscrow = signallingEscrow;
} else {
newSignallingEscrow = signallingEscrow;
newRageQuitEscrow = rageQuitEscrow;
}

STORAGE_SETUP.dualGovernanceInitializeStorage(dualGovernance, newSignallingEscrow, newRageQuitEscrow);

if (transitionToRageQuit) {
vm.assume(dualGovernance.getCurrentState() == State.RageQuit);
}

STORAGE_SETUP.signallingEscrowInitializeStorage(newSignallingEscrow, dualGovernance);
STORAGE_SETUP.rageQuitEscrowInitializeStorage(newRageQuitEscrow, dualGovernance);
vm.assume(_getLastAssetsLockTimestamp(signallingEscrow, USER) < timeUpperBound);

{
uint128 senderLockedShares = uint128(kevm.freshUInt(16));
vm.assume(senderLockedShares < ethUpperBound);
uint128 senderUnlockedShares = uint128(kevm.freshUInt(16));
bytes memory slotAbi = abi.encodePacked(uint128(senderUnlockedShares), uint128(senderLockedShares));
bytes32 slot;
assembly {
slot := mload(add(slotAbi, 0x20))
}
_storeBytes32(
address(signallingEscrow),
93842437974268059396725027201531251382101332839645030345425397622830526343272,
slot
);
}

AccountingRecord memory post = STORAGE_SETUP.saveAccountingRecord(USER, signallingEscrow);

STORAGE_SETUP.establishEqualAccountingRecords(Mode.Assume, pre, post);
}
}

Expand Down
74 changes: 68 additions & 6 deletions test/kontrol/EscrowLockUnlock.t.sol
View file
Original file line number Diff line number Diff line change
Expand Up @@ -90,7 +90,7 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp {
this.signallingEscrowInvariants(Mode.Assume, signallingEscrow);
this.escrowUserInvariants(Mode.Assume, signallingEscrow, sender);

ActivateNextStateMock mock = new ActivateNextStateMock(address(this));
ActivateNextStateMock mock = new ActivateNextStateMock(address(this), sender);
kevm.mockFunction(
address(dualGovernance), address(mock), abi.encodeWithSelector(mock.activateNextState.selector)
);
Expand All @@ -117,10 +117,52 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp {

uint256 errorTerm = stEth.getPooledEthByShares(1) + 1;
assert(post.userBalance <= pre.userBalance - amount + errorTerm);
assert(pre.escrowBalance + amount < errorTerm || pre.escrowBalance + amount - errorTerm <= post.escrowBalance);
assert(pre.totalEth + amount < errorTerm || pre.totalEth + amount - errorTerm <= post.totalEth);
// Rewritten to avoid branching
//assert(pre.escrowBalance + amount < errorTerm || pre.escrowBalance + amount - errorTerm <= post.escrowBalance);
assert(pre.escrowBalance + amount <= post.escrowBalance + errorTerm);
// Rewritten to avoid branching
//assert(pre.totalEth + amount < errorTerm || pre.totalEth + amount - errorTerm <= post.totalEth);
assert(pre.totalEth + amount <= post.totalEth + errorTerm);
}

// Isolating individual branches of testUnlockStEth

function testUnlockStEth_1() public {
State initialState = dualGovernance.getCurrentState();

vm.assume(initialState != State.VetoSignalling);
vm.assume(initialState != State.VetoSignallingDeactivation);

testUnlockStEth();
}

function testUnlockStEth_2() public {
State initialState = dualGovernance.getCurrentState();
uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport();

vm.assume(initialState != State.Normal);
vm.assume(initialState != State.VetoCooldown);
vm.assume(initialState != State.RageQuit);
vm.assume(rageQuitSupport <= config.SECOND_SEAL_RAGE_QUIT_SUPPORT());

testUnlockStEth();
}

function testUnlockStEth_3() public {
State initialState = dualGovernance.getCurrentState();
uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport();
Timestamp vetoSignallingActivationTime = Timestamp.wrap(_getVetoSignallingActivationTime(dualGovernance));

vm.assume(initialState != State.Normal);
vm.assume(initialState != State.VetoCooldown);
vm.assume(initialState != State.RageQuit);
vm.assume(rageQuitSupport > config.SECOND_SEAL_RAGE_QUIT_SUPPORT());
vm.assume(Timestamps.now() <= config.DYNAMIC_TIMELOCK_MAX_DURATION().addTo(vetoSignallingActivationTime));

testUnlockStEth();
}

//
function testUnlockStEth() public {
// Placeholder address to avoid complications with keccak of symbolic addresses
address sender = address(uint160(uint256(keccak256("sender"))));
Expand All @@ -141,6 +183,7 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp {
);

uint128 senderLockedShares = uint128(kevm.freshUInt(16));
vm.assume(senderLockedShares < ethUpperBound);
uint128 senderUnlockedShares = uint128(kevm.freshUInt(16));
bytes memory slotAbi = abi.encodePacked(uint128(senderUnlockedShares), uint128(senderLockedShares));
bytes32 slot;
Expand Down Expand Up @@ -170,7 +213,22 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp {
this.signallingEscrowInvariants(Mode.Assume, signallingEscrow);
this.escrowUserInvariants(Mode.Assume, signallingEscrow, sender);

ActivateNextStateMock mock = new ActivateNextStateMock(address(this));
bool transitionToRageQuit;

{
State initialState = dualGovernance.getCurrentState();
uint256 rageQuitSupport = signallingEscrow.getRageQuitSupport();
Timestamp vetoSignallingActivationTime = Timestamp.wrap(_getVetoSignallingActivationTime(dualGovernance));

transitionToRageQuit = (
initialState == State.VetoSignalling || initialState == State.VetoSignallingDeactivation
) && rageQuitSupport > config.SECOND_SEAL_RAGE_QUIT_SUPPORT()
&& Timestamps.now() > config.DYNAMIC_TIMELOCK_MAX_DURATION().addTo(vetoSignallingActivationTime);
}

vm.assume(!transitionToRageQuit);

ActivateNextStateMock mock = new ActivateNextStateMock(address(this), sender);
kevm.mockFunction(
address(dualGovernance), address(mock), abi.encodeWithSelector(mock.activateNextState.selector)
);
Expand All @@ -192,10 +250,14 @@ contract EscrowLockUnlockTest is EscrowInvariants, DualGovernanceSetUp {
// Accounts for rounding errors in the conversion to and from shares
uint256 amount = stEth.getPooledEthByShares(pre.userSharesLocked);

assert(pre.escrowBalance - amount < 1 || pre.escrowBalance - amount - 1 <= post.escrowBalance);
// Rewritten to avoid branching
//assert(pre.escrowBalance - amount < 1 || pre.escrowBalance - amount - 1 <= post.escrowBalance);
assert(pre.escrowBalance - amount <= post.escrowBalance + 1);
assert(post.escrowBalance <= pre.escrowBalance - amount);

assert(pre.totalEth - amount < 1 || pre.totalEth - amount - 1 <= post.totalEth);
// Rewritten to avoid branching
//assert(pre.totalEth - amount < 1 || pre.totalEth - amount - 1 <= post.totalEth);
assert(pre.totalEth - amount <= post.totalEth + 1);
assert(post.totalEth <= pre.totalEth - amount);

assert(pre.userBalance + amount <= post.userBalance);
Expand Down

0 comments on commit ad10520

Please sign in to comment.