AtHeartEngineer/staking-reward-streamer
1
0
Fork 0
mirror of https://github.com/vacp2p/staking-reward-streamer.git synced 2026-01-09 15:27:55 -05:00
Code Issues Packages Projects Releases Wiki Activity

fix(certora): fix timeout on certora with specific config

Browse Source
This commit is contained in:
r4bbit
2025-03-07 12:00:43 +01:00
parent e4d21b6caf
commit 6c89793854
3 changed files with 44 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

35
certora/confs/MPLessEqualMaxMP.conf Normal file
View File

@@ -0,0 +1,35 @@
{
"files": [
"src/RewardsStreamerMP.sol",
"certora/helpers/ERC20A.sol"
],
"link": [
"RewardsStreamerMP:STAKING_TOKEN=ERC20A"
],
"loop_iter": "3",
"msg": "Verifying RewardsStreamerMP.sol",
"optimistic_loop": true,
"packages": [
"forge-std=lib/forge-std/src",
"@openzeppelin/contracts=lib/openzeppelin-contracts/contracts",
"@openzeppelin/contracts-upgradeable=lib/openzeppelin-contracts-upgradeable/contracts"
],
"process": "emv",
"prover_args": [
"-backendStrategy singleRace",
"-smt_useLIA false",
"-smt_useNIA true",
"-mediumTimeout 20",
"-lowTimeout 20",
"-tinyTimeout 20",
"-depth 20",
"-solvers [z3:def{randomSeed=11},z3:def{randomSeed=12},z3:def{randomSeed=13},z3:def{randomSeed=14},z3:def{randomSeed=15},z3:def{randomSeed=16},z3:def{randomSeed=17},z3:def{randomSeed=18},z3:def{randomSeed=19},z3:def{randomSeed=20}]"
],
"rule": [
"vaultMPLessEqualVaultMaxMP"
],
"rule_sanity": "basic",
"server": "production",
"verify": "RewardsStreamerMP:certora/specs/RewardsStreamerMP.spec"
}

7
certora/confs/RewardsStreamerMP.conf
View File

@@ -12,6 +12,13 @@
"optimistic_loop": true,
"loop_iter": "3",
"prover_args": ["-backendStrategy singleRace -smt_useLIA false -smt_useNIA true -depth 0 -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]"],
"rule": [
"sumOfBalancesIsTotalStaked",
"vaultMPGreaterEqualVaultStakedBalance",
"stakingMintsMultiplierPoints1To1Ratio",
"stakingGreaterLockupTimeMeansGreaterMPs",
"MPsOnlyDecreaseWhenUnstaking"
],
"packages": [
"forge-std=lib/forge-std/src",
"@openzeppelin/contracts=lib/openzeppelin-contracts/contracts",

3
package.json
View File

@@ -23,8 +23,9 @@
"scripts": {
"clean": "rm -rf cache out",
"lint": "pnpm lint:sol && pnpm prettier:check",
"verify": "pnpm verify:rewards_streamer_mp && pnpm verify:karma && pnpm verify:emergency_mode",
"verify": "pnpm verify:rewards_streamer_mp && pnpm verify:mp_less_equal_max_mp && pnpm verify:karma && pnpm verify:emergency_mode",
"verify:rewards_streamer_mp": "certoraRun certora/confs/RewardsStreamerMP.conf",
"verify:mp_less_equal_max_mp": "certoraRun certora/confs/MPLessEqualMaxMP.conf",
"verify:emergency_mode": "certoraRun certora/confs/EmergencyMode.conf",
"verify:karma": "certoraRun certora/confs/Karma.conf",
"lint:sol": "forge fmt --check && pnpm solhint {script,src,test,certora}/**/*.sol",