fix: certora prover ci (#477)

* fix: fallback args

* fix: updated storage syntax

Author: 8sunyuan

certora/scripts/core/verifyDelegationManager.sh

@@ -11,7 +11,7 @@ certoraRun certora/harnesses/DelegationManagerHarness.sol \
     src/contracts/core/Slasher.sol src/contracts/permissions/PauserRegistry.sol \
     --verify DelegationManagerHarness:certora/specs/core/DelegationManager.spec \
     --optimistic_loop \
-    --prover_args '-optimisticFallback true' \
+    --optimistic_fallback \
     --optimistic_hashing \
     --parametric_contracts DelegationManagerHarness \
     $RULE \

certora/scripts/core/verifyStrategyManager.sh

@@ -12,7 +12,7 @@ certoraRun certora/harnesses/StrategyManagerHarness.sol \
     src/contracts/core/Slasher.sol src/contracts/permissions/PauserRegistry.sol \
     --verify StrategyManagerHarness:certora/specs/core/StrategyManager.spec \
     --optimistic_loop \
-    --prover_args '-optimisticFallback true' \
+    --optimistic_fallback \
     --optimistic_hashing \
     --parametric_contracts StrategyManagerHarness \
     $RULE \

certora/scripts/libraries/verifyStructuredLinkedList.sh

@@ -8,7 +8,7 @@ solc-select use 0.8.12
 certoraRun certora/harnesses/StructuredLinkedListHarness.sol \
     --verify StructuredLinkedListHarness:certora/specs/libraries/StructuredLinkedList.spec \
     --optimistic_loop \
-    --prover_args '-optimisticFallback true' \
+    --optimistic_fallback \
     --parametric_contracts StructuredLinkedListHarness \
     $RULE \
     --rule_sanity \

certora/scripts/permissions/verifyPausable.sh

@@ -9,7 +9,8 @@ certoraRun certora/harnesses/PausableHarness.sol \
     src/contracts/permissions/PauserRegistry.sol \
     --verify PausableHarness:certora/specs/permissions/Pausable.spec \
     --optimistic_loop \
-    --prover_args '-optimisticFallback true -recursionErrorAsAssert false -recursionEntryLimit 3' \
+    --optimistic_fallback \
+    --prover_args '-recursionErrorAsAssert false -recursionEntryLimit 3' \
     --loop_iter 3 \
     --link PausableHarness:pauserRegistry=PauserRegistry \
     $RULE \

certora/scripts/pods/verifyEigenPodManager.sh

@@ -10,7 +10,7 @@ certoraRun certora/harnesses/EigenPodManagerHarness.sol \
     src/contracts/core/Slasher.sol src/contracts/permissions/PauserRegistry.sol \
     --verify EigenPodManagerHarness:certora/specs/pods/EigenPodManager.spec \
     --optimistic_loop \
-    --prover_args '-optimisticFallback true' \
+    --optimistic_fallback \
     --optimistic_hashing \
     --parametric_contracts EigenPodManagerHarness \
     $RULE \

certora/scripts/strategies/verifyStrategyBase.sh

@@ -12,7 +12,8 @@ certoraRun src/contracts/strategies/StrategyBase.sol \
     src/contracts/core/Slasher.sol \
     --verify StrategyBase:certora/specs/strategies/StrategyBase.spec \
     --optimistic_loop \
-    --prover_args '-optimisticFallback true -recursionErrorAsAssert false -recursionEntryLimit 3' \
+    --optimistic_fallback \
+    --prover_args '-recursionErrorAsAssert false -recursionEntryLimit 3' \
     --loop_iter 3 \
     --packages @openzeppelin=lib/openzeppelin-contracts @openzeppelin-upgrades=lib/openzeppelin-contracts-upgradeable \
     --link StrategyBase:strategyManager=StrategyManager \

certora/specs/libraries/StructuredLinkedList.spec

@@ -16,7 +16,7 @@ ghost mapping(uint256 => bool) connectsToHead {
     init_state axiom connectsToHead[0] == true;
 }
 
-hook Sstore currentContract.listStorage.list[KEY uint256 node][KEY bool direction] uint256 link (uint256 old_link) STORAGE {
+hook Sstore currentContract.listStorage.list[KEY uint256 node][KEY bool direction] uint256 link (uint256 old_link) {
     connectsToHead[link] = connectsToHead[node];
     connectsToHead[old_link] = old_link == 0;
 }

certora/specs/pods/EigenPod.spec

@@ -168,7 +168,7 @@ ghost mathint sumOfValidatorRestakedbalancesWei {
     init_state axiom sumOfValidatorRestakedbalancesWei == 0;
 }
 
-hook Sstore _validatorPubkeyHashToInfo[KEY bytes32 validatorPubkeyHash].restakedBalanceGwei uint64 newValue (uint64 oldValue) STORAGE {
+hook Sstore _validatorPubkeyHashToInfo[KEY bytes32 validatorPubkeyHash].restakedBalanceGwei uint64 newValue (uint64 oldValue) {
     sumOfValidatorRestakedbalancesWei = (
         sumOfValidatorRestakedbalancesWei + 
         to_mathint(newValue) * 1000000000 -