fix: failing certora-ci (#410)

* fix: try installing solc-select * fix: addShares selector
Layr-Labs · Feb 6, 2024 · 7511559 · 7511559
1 parent 5b15e1e
commit 7511559
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 6 deletions.
diff --git 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 }}

diff --git 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);