Correct.

Correct.

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.

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

Correct.

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.

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);
    }
    ```

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.

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)

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

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.

@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

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

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;