Exemplary ERC4626 specs #3
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…adding run script
# Conflicts: # lesson4_reading/erc4626/src/certora/specs/ERC4626-FunctionalAccountingProps.spec # lesson4_reading/erc4626/src/certora/specs/ERC4626-InflationAttack.spec # lesson4_reading/erc4626/src/certora/specs/ERC4626-MonotonicityInvariant.spec # lesson4_reading/erc4626/src/certora/specs/ERC4626-MustNotRevertProps.spec # lesson4_reading/erc4626/src/certora/specs/ERC4626-RoundingProps.spec # lesson4_reading/erc4626/src/certora/specs/ERC4626-SecurityProps.spec
…Run-RoundingProps.conf
…4382a1e75ffcaa6f23b8?anonymousKey=eaba7fbede3b755b6e06ccca83805caaddfb8e6f with arguments src/certora/conf-openzeppelin/certoraRun-RoundingProps.conf
…47af92ddfa2d475ff848?anonymousKey=434e0e7b5de57acf2a7535e7b89ad497b97ef7d1 with arguments src/certora/conf-openzeppelin/certoraRun-RoundingProps.conf
…Run-RoundingProps.conf
…4f88ad532931801f0535?anonymousKey=3668bd548cd9a7a132e1279f31076b14cc3a2ded with arguments src/certora/conf-openzeppelin/certoraRun-RoundingProps.conf
…4196b5440faf3da7e93c?anonymousKey=157ffed5e74f6268ac0b7885c76bd6e212dffd47 with arguments src/certora/conf-openzeppelin/certoraRun-RoundingProps.conf
…47e39db2c2116fbd2cab?anonymousKey=48f49e511bd937ecc77323388937c501971267d6 with arguments src/certora/conf-openzeppelin/certoraRun-RoundingProps.conf
…4a609bc9c957048b7a63?anonymousKey=4f05de0fb2412ff4376b913e8011d0fad264b633 with arguments src/certora/conf-openzeppelin/certoraRun-RoundingProps.conf
…406092616a327c3eb344?anonymousKey=f040208a3b062fb93dabf8a9b59cd55ec83df1c7 with arguments src/certora/conf-openzeppelin/certoraRun-RoundingProps.conf
…cessary rules for documentation purpose
…s of convertToAssets/convertToShares
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Adding ERC4626 specs that can be used as baseline for other ERC4626 implementations.