Governed Gas Pool Spec

[l-monninger]

Description

• Creates governed_gas_pool.spec.move
• Updated transaction_validation.spec.move

Type of Change

• New feature
• Bug fix
• Breaking change
• Performance improvement
• Refactoring
• Dependency update
• Documentation update
• Tests

Which Components or Systems Does This Change Impact?

• Validator Node
• Full Node (API, Indexer, etc.)
• Move/Aptos Virtual Machine
• Aptos Framework
• Aptos CLI/SDK
• Developer Infrastructure
• Other (specify)

How Has This Been Tested?

Yes

• aptos move prove -f governed_gas_pool && aptos move prove -f transaction_validation
• aptos move test`

Key Areas to Review

IMPORTANT
When the feature COIN_TO_FUNGIBLE_ASSET_MIGRATION is enabled, this causes the spec fund in governed_gas_pool.spec.move to fail. So, I disabled it and it passes as expected.

I would advise us to disable this feature for mainnet as it seems strange to enable as we are not migrating to FA yet. However, if we do want to go to mainnet with this feature enabled, then I would imagine something is wrong with the spec.

NOTE
When trying to call governed_gas_pool_address() within the governed_gas_pool spec I get the following error

{
  "Error": "Move Prover failed: [internal] boogie exited with compilation errors:\n/Users/movses/mvmt/mvmt-aptos-core/aptos-move/framework/aptos-framework/boogie.bpl(12265,39): Error: use of undeclared function: $1_create_signer_$create_signer\n1 name resolution errors detected in /Users/movses/mvmt/mvmt-aptos-core/aptos-move/framework/aptos-framework/boogie.bpl\n"
}

@franck44 mentions this is a problem to do with versioning and configuration. I tried it with both aptos move prove and movement move prove, but it yields the same result. From the error message it seems that Boogie doesn't have a declaration for create_signer at runtime. So making ensures for resource accounts seems tricky.

In any case the changes offered here offer some value toward full verification.

[l-monninger]

Correct.

[l-monninger]

Correct.

[l-monninger]

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.

[0xmovses]

When I try to to do ensures with anything resource account related I get the error noted down in the PR description.

[l-monninger]

Correct.

[l-monninger]

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.

[0xmovses]

It's passing though, I think because of

spec initialize(aptos_framework: &signer, delegation_pool_creation_seed: vector<u8>) {
        requires system_addresses::is_aptos_framework_address(signer::address_of(aptos_framework));
        /// [high-level-req-1]
        ensures exists<GovernedGasPool>(@aptos_framework);
    }
    ```

[0xmovses]

I can remove it if you we prefer. I suppose we would need to be doing an init_module for it to be an invariant.

[l-monninger]

@0xmovses do you have any of the transaction_fee.spec.move or transaction_validation.spec.move written out?

[0xmovses]

@l-monninger Yes the changes for transaction_validation.spec.move are in the PR and passing. What you had commented, that logic is now running in the prover an passing.

[l-monninger]

This is the critical bit to validate. But, you'll notice Aptos has not made the effort to prove that herein since the FA migration began and instead would do it in transaction_fee.spec.move

This is what I was commenting on here: #114 (comment)

[l-monninger]

@franck44 Can you comment here on the difference in approaches used in transaction_validation.spec.move and transaction_fee.spec.move?

[0xmovses]

Yes, I had done this earlier:

public fun coin_to_fungible_asset_migration_feature_enabled(): bool {
       false 
  }

Which if I remember correctly, made this line pass. But with the feature enabled, I am not able to make ensures on coin, because the migration paths are hit at run time.

I though it better to keep that feature in. We could decide not to enable this feature, then we would have more verification.

[l-monninger]

@0xmovses So, you're saying that this all should pass if I hardcode as suggested here?: https://github.com/movementlabsxyz/aptos-core/pull/118/files/8c8ce6c47e48a0cd786f000cdd7714b2671182db#r1907843043

[0xmovses]

With the feature disabled like this:

public fun coin_to_fungible_asset_migration_feature_enabled(): bool {
        false
        //is_enabled(COIN_TO_FUNGIBLE_ASSET_MIGRATION) 
    }

then the L293 & 294 for transaction_validation.spec.move pass :

let pre_governed_gas_pool_balance = global<coin::CoinStore<AptosCoin>>(governed_gas_pool_address()).coin.value;
let post governed_gas_pool_balance = global<coin::CoinStore<AptosCoin>>(governed_gas_pool_address()).coin.value;

aptos move prove -f aptos move prove -f transaction_validation

Furthermore more can be verified within governed_gas_pool.spec.move

[0xmovses]

Forgot to add and these two lines, to comment out, these ensures pass

ensures governed_gas_pool_balance == pre_governed_gas_pool_balance + transaction_fee_amount;
ensures account.sequence_number == pre_account.sequence_number + 1;