Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore(StakeManagerProcessAccount.spec): add specs for processAccount #57

Merged
merged 1 commit into from
Mar 18, 2024

Conversation

0x-r4bbit
Copy link
Collaborator

Checklist

Ensure you completed all of the steps below before submitting your pull request:

  • Added natspec comments?
  • Ran forge snapshot?
  • Ran pnpm lint?
  • Ran forge test?
  • Ran pnpm verify?

This primarily adds a rule that ensures that, when an account's
`balance` changes, `_processAccount()` must have been called as well.

There's very few exceptions where an account's `balance` can change
without the need of `_processAccount()` but those functions have been
deliberately excluded from the rule.
@0x-r4bbit 0x-r4bbit changed the base branch from chore/certora-setup to develop March 13, 2024 11:37

// If the account's `lockUntil` == 0, then the account will be initialized
// with the current epoch and no processing is required.
require getAccountLockUntil(account) > 0;
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ha, this was a tricky one to find.
Was debugging a counter example, without realizing that the accountProcessed ghost was never touched.

@0x-r4bbit 0x-r4bbit requested a review from 3esmit March 13, 2024 11:39
@0x-r4bbit
Copy link
Collaborator Author

@3esmit re-requesting review on this one.

I've finally managed to get this one pass. However, I've changed the base branch of this PR after I've pushed my update, so the CI actions aren't triggered.

I've triggered them manually here: https://github.com/logos-co/staking/actions/runs/8264004339

@0x-r4bbit
Copy link
Collaborator Author

This has been sitting here for almost a week since a re-review was requested.
Since the corresponding job ( https://github.com/logos-co/staking/actions/runs/8264004339) is green, I"m going to merge this one.

@0x-r4bbit 0x-r4bbit merged commit 70b092a into develop Mar 18, 2024
7 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants