0xmovses/goverened gas pool spec #118
Open
Conversation
This file contains 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
l-monninger
commented
Jan 3, 2025
| spec aptos_framework::governed_gas_pool { | ||
| /// <high-level-req> | ||
| /// No.: 1 | ||
| /// Requirement: The GovernedGasPool resource must exist at the aptos_framework address after initialization. |
| /// Enforcement: Formally verified via [high-level-req-1](initialize). | ||
| /// | ||
| /// No.: 2 | ||
| /// Requirement: Only the aptos_framework address is allowed to initialize the GovernedGasPool. |
| /// Enforcement: Formally verified via [high-level-req-2](initialize). | ||
| /// | ||
| /// No.: 3 | ||
| /// Requirement: Deposits into the GovernedGasPool must be reflected in the pool's balance. |
There was a problem hiding this comment.
I would say you want to prove above that initialization creates a resource account distinct from the aptos_framework address. Then deposits into the GovernedGasPool are reflected in that account's balance.
| /// Enforcement: Formally verified via [high-level-req-3](deposit), [high-level-req-3.1](deposit_from). | ||
| /// | ||
| /// No.: 4 | ||
| /// Requirement: Only the aptos_framework address can fund accounts from the GovernedGasPool. |
| /// Enforcement: Formally verified via [high-level-req-4](fund). | ||
| /// | ||
| /// No.: 5 | ||
| /// Requirement: Gas fees must be deposited into the GovernedGasPool whenever specified by the configuration. |
There was a problem hiding this comment.
This is a requirement on transaction_validation.spec.move or transaction_fee.spec.move.
| spec module { | ||
| /// [high-level-req-1] | ||
| /// The GovernedGasPool resource must exist at aptos_framework after initialization. | ||
| invariant exists<GovernedGasPool>(@aptos_framework); |
There was a problem hiding this comment.
The GovernGasPool exists for the aptos_framework cannot be an invariant. You would need an exists implies, i.e., ==>. One thing the GovernedGasPool existing could imply is that the resource account for the GovernedGasPool exists.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Description
Type of Change
Which Components or Systems Does This Change Impact?
How Has This Been Tested?
Key Areas to Review
Checklist