From 741f39f0bcc6aa330e14e9a91d1cb72131c4e60e Mon Sep 17 00:00:00 2001 From: F-WRunTime Date: Wed, 12 Jun 2024 14:31:40 -0600 Subject: [PATCH 1/9] Committing KaaS Compute Setup for RV Testing / Development --- .github/workflows/lido-ci.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/lido-ci.yml b/.github/workflows/lido-ci.yml index 9d60dea3..7e3386e7 100644 --- a/.github/workflows/lido-ci.yml +++ b/.github/workflows/lido-ci.yml @@ -23,13 +23,13 @@ -H "Authorization: Bearer ${{ secrets.RV_COMPUTE_TOKEN }}" \ https://api.github.com/repos/runtimeverification/_kaas_lidofinance_dual-governance/actions/workflows/lido-ci.yml/dispatches \ -d '{ - "ref": "master", + "ref": "rvdevelop", "inputs": { "branch_name": "'"${{ github.event.pull_request.head.sha || github.sha }}"'", "extra_args": "script", "statuses_sha": "'$sha'", - "org": "lidofinance", - "repository": "dual-governance", + "org": "runtimeverification", + "repository": "_audits_lidofinance_dual-governance_fork", "auth_token": "'"${{ secrets.LIDO_STATUS_TOKEN }}"'" } }') From 7a51acf740d23c89894032ac4516919fe7639298 Mon Sep 17 00:00:00 2001 From: F-WRunTime Date: Wed, 12 Jun 2024 14:39:01 -0600 Subject: [PATCH 2/9] Test using variables to get org name / repo name --- .github/workflows/lido-ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/lido-ci.yml b/.github/workflows/lido-ci.yml index 7e3386e7..264805d3 100644 --- a/.github/workflows/lido-ci.yml +++ b/.github/workflows/lido-ci.yml @@ -28,8 +28,8 @@ "branch_name": "'"${{ github.event.pull_request.head.sha || github.sha }}"'", "extra_args": "script", "statuses_sha": "'$sha'", - "org": "runtimeverification", - "repository": "_audits_lidofinance_dual-governance_fork", + "org": "${{ github.repository_owner }}", + "repository": "${{ github.event.repository.name }}", "auth_token": "'"${{ secrets.LIDO_STATUS_TOKEN }}"'" } }') From 60eebbb5aa6e8c790b0f9c5dbdc83a1dceda5e79 Mon Sep 17 00:00:00 2001 From: Freeman <105403280+F-WRunTime@users.noreply.github.com> Date: Wed, 12 Jun 2024 14:55:02 -0600 Subject: [PATCH 3/9] Update lido-ci.yml --- .github/workflows/lido-ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/lido-ci.yml b/.github/workflows/lido-ci.yml index 264805d3..ebcf2963 100644 --- a/.github/workflows/lido-ci.yml +++ b/.github/workflows/lido-ci.yml @@ -3,7 +3,7 @@ on: pull_request: branches: - - main + - develop jobs: test: runs-on: ubuntu-latest From 5070a16404bb21a6e1762405f09b25f58f5a9d48 Mon Sep 17 00:00:00 2001 From: F-WRunTime Date: Wed, 12 Jun 2024 15:12:10 -0600 Subject: [PATCH 4/9] Merge conflict resolution --- .github/workflows/lido-ci.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/lido-ci.yml b/.github/workflows/lido-ci.yml index ebcf2963..1ff7f9f5 100644 --- a/.github/workflows/lido-ci.yml +++ b/.github/workflows/lido-ci.yml @@ -1,9 +1,10 @@ --- name: "Test Proofs" on: - pull_request: + push: branches: - develop + - rvdevelop jobs: test: runs-on: ubuntu-latest From fb685aa6839fcc304ebc1a8739da0d82e8c6ddc8 Mon Sep 17 00:00:00 2001 From: lucasmt Date: Wed, 12 Jun 2024 13:37:22 -0500 Subject: [PATCH 5/9] Add separate profile for kontrol proofs --- foundry.toml | 6 ++++++ test/kontrol/scripts/run-kontrol.sh | 4 ++-- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/foundry.toml b/foundry.toml index 168aec6d..196e3fca 100644 --- a/foundry.toml +++ b/foundry.toml @@ -5,6 +5,12 @@ libs = ['node_modules', 'lib'] test = 'test' cache_path = 'cache_forge' solc-version = "0.8.23" +no-match-path = 'test/kontrol/*' + +[profile.kprove] +src = 'test/kontrol' +out = 'kout' +test = 'test/kontrol' [fmt] multiline_func_header = 'params_first' diff --git a/test/kontrol/scripts/run-kontrol.sh b/test/kontrol/scripts/run-kontrol.sh index d649f2d8..cd055976 100755 --- a/test/kontrol/scripts/run-kontrol.sh +++ b/test/kontrol/scripts/run-kontrol.sh @@ -5,9 +5,9 @@ SCRIPT_HOME="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" # shellcheck source=/dev/null source "$SCRIPT_HOME/common.sh" export RUN_KONTROL=true -CUSTOM_FOUNDRY_PROFILE=default +CUSTOM_FOUNDRY_PROFILE=kprove export FOUNDRY_PROFILE=$CUSTOM_FOUNDRY_PROFILE -export OUT_DIR=out # out dir of $FOUNDRY_PROFILE +export OUT_DIR=kout # out dir of $FOUNDRY_PROFILE parse_args "$@" ############# From 0e48f528cd6677ead9c9c7113b653261e40bdec6 Mon Sep 17 00:00:00 2001 From: lucasmt Date: Wed, 12 Jun 2024 15:28:49 -0500 Subject: [PATCH 6/9] Update model --- contracts/model/DualGovernance.sol | 11 +++++------ contracts/model/EmergencyProtectedTimelock.sol | 2 -- 2 files changed, 5 insertions(+), 8 deletions(-) diff --git a/contracts/model/DualGovernance.sol b/contracts/model/DualGovernance.sol index 5ab56511..490378ac 100644 --- a/contracts/model/DualGovernance.sol +++ b/contracts/model/DualGovernance.sol @@ -1,6 +1,8 @@ // SPDX-License-Identifier: MIT pragma solidity ^0.8.0; +import "@openzeppelin/contracts/utils/math/Math.sol"; + import "./EmergencyProtectedTimelock.sol"; import "./Escrow.sol"; @@ -84,8 +86,9 @@ contract DualGovernance { "Proposals can only be scheduled in Normal or Veto Cooldown states." ); if (currentState == State.VetoCooldown) { + uint256 submissionTime = emergencyProtectedTimelock.proposals(proposalId).submissionTime; require( - block.timestamp < lastVetoSignallingTime, + submissionTime < lastVetoSignallingTime, "Proposal submitted after the last time Veto Signalling state was entered." ); } @@ -174,10 +177,6 @@ contract DualGovernance { currentState = parentState; } - function max(uint256 a, uint256 b) private pure returns (uint256) { - return a > b ? a : b; - } - // State Transitions function activateNextState() public { @@ -231,7 +230,7 @@ contract DualGovernance { transitionState(State.RageQuit); } else if ( block.timestamp - lastStateChangeTime > calculateDynamicTimelock(rageQuitSupport) - && block.timestamp - max(lastStateChangeTime, lastStateReactivationTime) + && block.timestamp - Math.max(lastStateChangeTime, lastStateReactivationTime) > VETO_SIGNALLING_MIN_ACTIVE_DURATION ) { enterSubState(State.VetoSignallingDeactivation); diff --git a/contracts/model/EmergencyProtectedTimelock.sol b/contracts/model/EmergencyProtectedTimelock.sol index df673108..f63bd6c9 100644 --- a/contracts/model/EmergencyProtectedTimelock.sol +++ b/contracts/model/EmergencyProtectedTimelock.sol @@ -55,8 +55,6 @@ contract EmergencyProtectedTimelock { function submit(address executor, ExecutorCall[] memory calls) external returns (uint256 proposalId) { // Ensure that only the governance can submit new proposals. require(msg.sender == governance, "Only governance can submit proposal."); - // Establish the minimum timelock duration for the proposal's execution. - uint256 executionDelay = PROPOSAL_EXECUTION_MIN_TIMELOCK; proposals[nextProposalId].id = nextProposalId; proposals[nextProposalId].proposer = executor; From 246d5f85f3ebdada5664783e5b0e92f6fba93b3b Mon Sep 17 00:00:00 2001 From: lucasmt Date: Wed, 12 Jun 2024 14:17:20 -0500 Subject: [PATCH 7/9] Fix VetoSignalling tests --- test/kontrol/VetoSignalling.t.sol | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/test/kontrol/VetoSignalling.t.sol b/test/kontrol/VetoSignalling.t.sol index 2451de91..0db58bd3 100644 --- a/test/kontrol/VetoSignalling.t.sol +++ b/test/kontrol/VetoSignalling.t.sol @@ -26,7 +26,7 @@ contract VetoSignallingTest is Test, KontrolCheats { // Note: there are lemmas dependent on `ethUpperBound` uint256 constant ethMaxWidth = 96; uint256 constant ethUpperBound = 2 ** ethMaxWidth; - uint256 constant timeUpperBound = 2 ** 40 - 1; + uint256 constant timeUpperBound = 2 ** 40; enum Mode { Assume, @@ -150,7 +150,7 @@ contract VetoSignallingTest is Test, KontrolCheats { _storeUInt256(address(rageQuitEscrow), 5, totalClaimedEthAmount); // Slot 11 uint256 rageQuitExtensionDelayPeriodEnd = kevm.freshUInt(32); // ?WORD10 - _storeUInt256(address(signallingEscrow), 11, rageQuitExtensionDelayPeriodEnd); + _storeUInt256(address(rageQuitEscrow), 11, rageQuitExtensionDelayPeriodEnd); } function _storeBytes32(address contractAddress, uint256 slot, bytes32 value) internal { @@ -345,15 +345,6 @@ contract VetoSignallingTest is Test, KontrolCheats { vm.assume(previousRageQuitSupport < ethUpperBound); vm.assume(maxRageQuitSupport < ethUpperBound); - // Temporary assumptions - vm.assume(previousRageQuitSupport <= 1); - vm.assume(10 <= maxRageQuitSupport); - vm.assume( - lastInteractionTimestamp - <= dualGovernance.lastStateChangeTime() + dualGovernance.calculateDynamicTimelock(previousRageQuitSupport) - ); - // Temparary assumptions - StateRecord memory previous = _recordPreviousState(lastInteractionTimestamp, previousRageQuitSupport, maxRageQuitSupport); @@ -385,9 +376,12 @@ contract VetoSignallingTest is Test, KontrolCheats { uint256 previousRageQuitSupport, uint256 maxRageQuitSupport ) external { + vm.assume(block.timestamp < timeUpperBound); + StateRecord memory previous = _recordPreviousState(lastInteractionTimestamp, previousRageQuitSupport, maxRageQuitSupport); + vm.assume(previous.maxRageQuitSupport <= dualGovernance.SECOND_SEAL_RAGE_QUIT_SUPPORT()); vm.assume(_maxDeactivationDelayPassed(previous)); vm.assume(signallingEscrow.getRageQuitSupport() <= previous.maxRageQuitSupport); From 699ed04da1508b6997ed4c7fcea0abdcad4f4750 Mon Sep 17 00:00:00 2001 From: lucasmt Date: Wed, 12 Jun 2024 17:30:59 -0500 Subject: [PATCH 8/9] Fix check in Escrow model --- contracts/model/Escrow.sol | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/contracts/model/Escrow.sol b/contracts/model/Escrow.sol index 900ebe71..cb256e30 100644 --- a/contracts/model/Escrow.sol +++ b/contracts/model/Escrow.sol @@ -67,7 +67,7 @@ contract Escrow { require(currentState == State.SignallingEscrow, "Cannot lock in current state."); require(amount > 0, "Amount must be greater than zero."); require(fakeETH.allowance(msg.sender, address(this)) >= amount, "Need allowance to transfer tokens."); - require(fakeETH.balanceOf(msg.sender) <= amount, "Not enough balance."); + require(fakeETH.balanceOf(msg.sender) >= amount, "Not enough balance."); fakeETH.transferFrom(msg.sender, address(this), amount); balances[msg.sender] += amount; totalStaked += amount; From ac35908ee6f6e6057a6ac99ce0f94dc04f7223f4 Mon Sep 17 00:00:00 2001 From: lucasmt Date: Wed, 12 Jun 2024 16:40:58 -0500 Subject: [PATCH 9/9] Revert changes to lido-ci.yml for merge into parent repo --- .github/workflows/lido-ci.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/lido-ci.yml b/.github/workflows/lido-ci.yml index 1ff7f9f5..2b4f13ad 100644 --- a/.github/workflows/lido-ci.yml +++ b/.github/workflows/lido-ci.yml @@ -4,7 +4,6 @@ push: branches: - develop - - rvdevelop jobs: test: runs-on: ubuntu-latest @@ -24,7 +23,7 @@ -H "Authorization: Bearer ${{ secrets.RV_COMPUTE_TOKEN }}" \ https://api.github.com/repos/runtimeverification/_kaas_lidofinance_dual-governance/actions/workflows/lido-ci.yml/dispatches \ -d '{ - "ref": "rvdevelop", + "ref": "develop", "inputs": { "branch_name": "'"${{ github.event.pull_request.head.sha || github.sha }}"'", "extra_args": "script",