From 4a3166ab08ce6f597b9bad7e4476791965ba2073 Mon Sep 17 00:00:00 2001 From: 8sunyuan Date: Tue, 30 Jan 2024 10:32:37 -0500 Subject: [PATCH 1/2] fix: try installing solc-select --- .github/workflows/certora-prover.yml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/.github/workflows/certora-prover.yml b/.github/workflows/certora-prover.yml index 868addac1..e255d8e29 100644 --- a/.github/workflows/certora-prover.yml +++ b/.github/workflows/certora-prover.yml @@ -46,9 +46,8 @@ jobs: run: pip install certora-cli - name: Install solc run: | - wget https://github.com/ethereum/solidity/releases/download/v0.8.12/solc-static-linux - sudo mv solc-static-linux /usr/local/bin/solc - chmod +x /usr/local/bin/solc + pip install solc-select + solc-select use 0.8.12 --always-install - name: Verify rule ${{ matrix.params }} run: | bash ${{ matrix.params }} From a9b958f1af1f0252201b908939e814edda170f14 Mon Sep 17 00:00:00 2001 From: 8sunyuan Date: Tue, 6 Feb 2024 13:35:42 -0500 Subject: [PATCH 2/2] fix: addShares selector --- certora/specs/core/StrategyManager.spec | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/certora/specs/core/StrategyManager.spec b/certora/specs/core/StrategyManager.spec index ec7f7b9cd..43cd8e20f 100644 --- a/certora/specs/core/StrategyManager.spec +++ b/certora/specs/core/StrategyManager.spec @@ -20,7 +20,7 @@ methods { // external calls to StrategyManager function _.getDeposits(address) external => DISPATCHER(true); function _.slasher() external => DISPATCHER(true); - function _.addShares(address,address,uint256) external => DISPATCHER(true); + function _.addShares(address,address,address,uint256) external => DISPATCHER(true); function _.removeShares(address,address,uint256) external => DISPATCHER(true); function _.withdrawSharesAsTokens(address, address, uint256, address) external => DISPATCHER(true); @@ -97,7 +97,7 @@ definition methodCanIncreaseShares(method f) returns bool = f.selector == sig:depositIntoStrategy(address,address,uint256).selector || f.selector == sig:depositIntoStrategyWithSignature(address,address,uint256,address,uint256,bytes).selector || f.selector == sig:withdrawSharesAsTokens(address,address,uint256,address).selector - || f.selector == sig:addShares(address,address,uint256).selector; + || f.selector == sig:addShares(address,address,address,uint256).selector; /** * a staker's amount of shares in a strategy (i.e. `stakerStrategyShares[staker][strategy]`) should only decrease when @@ -129,7 +129,7 @@ rule newSharesIncreaseTotalShares(address strategy) { uint256 stakerStrategySharesBefore = get_stakerStrategyShares(e.msg.sender, strategy); uint256 totalSharesBefore = totalShares(strategy); if ( - f.selector == sig:addShares(address, address, uint256).selector + f.selector == sig:addShares(address, address, address, uint256).selector || f.selector == sig:removeShares(address, address, uint256).selector ) { uint256 totalSharesAfter = totalShares(strategy);