mirror of
https://github.com/vacp2p/staking-reward-streamer.git
synced 2026-01-09 13:08:03 -05:00
82c68c8b17
Most of the reasoning has been discussed in #208. Primarily what's happening here is: - `StakeManager.VaultData.lockUntil` has been removed - `StakeVault.lockUntil` has been introduced - `StakeVault.updateLockUntil(uint256 value)` has been introduced - `StakeVault.leave()` performs normal `leave()` action but keeps funds in vault if lockup period hasn't expired - `StakeVault.withdrawFromVault()` has been introduced to withdraw remaining *stake* funds in vault BREAKING CHANGE: - `StakeManager.VaultData.lockUntil` has been removed - `StakeVault.lockUntil` has been introduced - `StakeVault.leave()` performs normal `leave()` action but keeps funds in vault if lockup period hasn't expired Closes #208
39 lines
1.1 KiB
Plaintext
39 lines
1.1 KiB
Plaintext
{
|
|
"files": [
|
|
"src/StakeVault.sol",
|
|
"src/StakeManager.sol",
|
|
"certora/helpers/ERC20A.sol",
|
|
"certora/harness/StakeManagerHarness.sol"
|
|
],
|
|
"link": [
|
|
"StakeManagerHarness:STAKING_TOKEN=ERC20A"
|
|
],
|
|
"loop_iter": "3",
|
|
"msg": "Verifying StakeManager.sol",
|
|
"optimistic_loop": true,
|
|
"parametric_contracts": ["StakeManagerHarness"],
|
|
"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": "StakeManagerHarness:certora/specs/StakeManager.spec"
|
|
}
|
|
|