{
  "files":
    ["contracts/StakeManager.sol",
      "certora/helpers/ERC20A.sol",
      "certora/helpers/StakeRewardEstimateA.sol"
    ],
  "link" : [
    "StakeManager:stakedToken=ERC20A",
    "StakeManager:stakeRewardEstimate=StakeRewardEstimateA"
  ],
  "msg": "Verifying StakeManager ProcessAccount",
  "rule_sanity": "basic",
  "verify": "StakeManager:certora/specs/StakeManagerProcessAccount.spec",
  "optimistic_loop": true,
  "loop_iter": "3",
  "packages": [
    "forge-std=lib/forge-std/src",
    "@openzeppelin=lib/openzeppelin-contracts"
  ]
}