Skip to content

[Certora] feat: Skim#887

Merged
QGarchery merged 45 commits intomainfrom
certora/skimming
Mar 5, 2026
Merged

[Certora] feat: Skim#887
QGarchery merged 45 commits intomainfrom
certora/skimming

Conversation

@bhargavbh
Copy link
Contributor

@bhargavbh bhargavbh commented Jan 26, 2026

properties verified separately for MarketV1AdapterV2 and VaultV1Adapter

  • skim() does not change vault accounting, i.e., vault funds can't be stolen by skimming
  • revert conditions for setSkimRecipient()

@bhargavbh bhargavbh self-assigned this Jan 26, 2026
@bhargavbh bhargavbh changed the title skim does not change realAssets [Certora] feat: Skim Jan 26, 2026
@bhargavbh bhargavbh marked this pull request as ready for review February 2, 2026 16:54
@bhargavbh bhargavbh requested a review from QGarchery February 16, 2026 15:29
Copy link
Collaborator

@jhoenicke jhoenicke left a comment

Choose a reason for hiding this comment

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

You should either havoc ghostBalances in the token transfer function, or use a nondet value instead of a ghost function. Otherwise the ghostBalances don't change on transfer.

@QGarchery QGarchery requested a review from jhoenicke February 23, 2026 09:10
Copy link
Collaborator

@jhoenicke jhoenicke left a comment

Choose a reason for hiding this comment

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

Some minor typos.
Otherwise the rules look fine.

@bhargavbh
Copy link
Contributor Author

@jhoenicke thanks, the minor issues are ironed out, should be good to merge after @MathisGD review

@lilCertora
Copy link
Collaborator

LGTM, still some typos to fix and ghostBalanceOf to be removed

@jhoenicke
Copy link
Collaborator

Looks like your last commit removed also adapterBalanceOf, but that is still needed by the spec.

@bhargavbh
Copy link
Contributor Author

@jhoenicke indeed, i think it should be good now

Copy link
Collaborator

@jhoenicke jhoenicke left a comment

Choose a reason for hiding this comment

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

All good now

@QGarchery QGarchery merged commit fc741f5 into main Mar 5, 2026
48 checks passed
@QGarchery QGarchery deleted the certora/skimming branch March 5, 2026 13:58
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.

5 participants