Skip to content

Conversation

@tosofia
Copy link
Contributor

@tosofia tosofia commented Mar 16, 2025

Changes to deposit_erc20 contract:

  • renamed no-deposit-twice in deposit-deposit-revert
  • added new properties (always-depletable, no-deposit-twice, wd-not-revert and wd-sender-rcv)
  • added certora conf files
  • added helper to setup certora dispatcher
  • added hardhat poc for wd-leq-init-bal property

Copy link
Owner

@fsainas fsainas left a comment

Choose a reason for hiding this comment

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

Hello,

It seems this use case doesn't fully follow the standard. The Makefile differs from the one in the template directory, and getters.sol and methods.sol are missing from the Certora directory. Lastly, it seems the Hardhat proof of concept is missing from the changes. Please refer to the README for the exhaustive use case specification and update the PR accordingly.

Thanks!

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.

3 participants