[Prover]Proving properties about data structures containing AptosCoin

[weeafoov]

Discord user ID

No response

Describe your question in detail.

I have some troubles understanding why I can't prove my
code specification with move prover:

What I am trying to do:
Two things:

1. Implement a simple (toy example) Bank where:
   state is represented by a SimpleMap pairing addresses and AptosCoin
   and the only allowed action are:

• withdraw, which allows to transfer AptosCoin coins from an address
  inside a SimpleMap to an account
• deposit, which allows to deposit AptosCoin coins inside the SimpleMap
  at the address of the signer of the transaction

2. proving some simple properties, for example:

• When it aborts
• after a withdraw call the amount of AptosCoin of signer is increased by amount
• after a deposit call the amount of AptosCoin inside the SimpleMap is increased
  by amount deposited

full code of this can be found here

I am stuck on the initial step of the proving part, namely to precisely define all
the "aborts if" condition.

Errors (see also the error files in the "What error, if any, are you getting?" and steps to reproduce in "What have you tried or looked at? Or how can we reproduce the error?" below):

• prover tells me that the following do not abort: aborts_if !coin::spec_is_account_registered<coin::CoinStore>(signer::address_of(client));
  (but should not be the case?, if I do understand, if a coin is not registerd to an account the procedure should abort?)

same for the following:
aborts_if !coin::is_coin_initialized<coin::CoinStore>();

aborts_if global<coin::CoinStore>(signer::address_of(client)).frozen;
(if an account coin store is frozen, should any deposit/withdraw fails?)

aborts_if global<coin::CoinStore>(signer::address_of(client)).coin.value + amount > MAX_U64;
(not sure if i have defined the property right: informally the function should abort if the amount withdrawn added with the current aptos coin held by the withdrawer is greater than the max value allowed, MAX_U64)

and the prover says that the following is not covered by the aborts_if guards
assert!(is_coin_initialized(), error::invalid_argument(ECOIN_INFO_NOT_PUBLISHED));

but I don't understand why this is not covered by the following:
aborts_if !coin::is_coin_initialized<coin::CoinStore>();

Also:

• I am a beginner on Move on Aptos, so any suggestions on how to
  structure/improve the code are welcome!
• If this is not the right place for asking such questions, please tell me so!
  (and sorry)

The bank code:
``

module bank_apt::bank {
use std::coin::{Self,Coin};
use aptos_framework::aptos_coin::AptosCoin;
use aptos_framework::aptos_account;
use std::signer;
use std::simple_map::{Self, SimpleMap};
// use aptos_std::type_info;
// mapping users -> coin(amount)
// using default coin since 
// transaction with generics are not
// supported apparently
struct Bank has key, store {
    clients : SimpleMap<address, Coin<AptosCoin>>,
}

const EAmountIsZero : u64 = 0;
const ENoAccount : u64 = 1;

// guaranteed to be called once only
// by move on aptos rule
fun init_module(account : &signer) {
    let bank = Bank{
        clients : simple_map::new()
    };
    move_to(account,bank);
}

// deposit is allowed only to the signer of the transaction (consistently with solidity implementation)
public entry fun deposit(to : &signer, bank : address, amount : u64) acquires Bank  {
    // do not allow pointless deposits
    assert!(amount != 0, EAmountIsZero);
    let deposit : Coin<AptosCoin> = coin::withdraw(to,amount);
    let bank = borrow_global_mut<Bank>(bank); 
    if (simple_map::contains_key(&bank.clients,&signer::address_of(to))){
        // exists already the account
        // so the new coin balance
        // must be the sum of the current balance + the old balance
        let coin_available = simple_map::borrow_mut(&mut bank.clients, &signer::address_of(to));
        coin::merge(coin_available,deposit); 
    } else {
        // balance does not exists already
        // initialize the account with 
        // the money deposited

        simple_map::add(&mut bank.clients, signer::address_of(to), deposit);
    }
}
//
public entry fun withdraw(client : &signer, bank : address, amount : u64) acquires Bank {
    // do not withdraw 0 
    assert!(amount != 0,EAmountIsZero);
    let bank = borrow_global_mut<Bank>(bank);
    let current_balance = simple_map::borrow_mut(&mut bank.clients, &signer::address_of(client));
    let withdrawn = coin::extract(current_balance,amount);
    // coin::deposit(signer::address_of(client), withdrawn);
    aptos_account::deposit_coins<AptosCoin>(signer::address_of(client),withdrawn);
}

#[test_only]
public fun test_init_module(initiator : &signer){
    init_module(initiator);
}
#[test_only]
public fun bank_exists(initiator : &signer) : bool {
    exists<Bank>(signer::address_of(initiator))
}
#[test_only]
public fun account_balance(account : &signer, bank : address) : u64 acquires Bank {
    let bank = borrow_global<Bank>(bank);
    let balance = simple_map::borrow(&bank.clients,&signer::address_of(account));
    coin::value(balance)
}

}

``

And the spec

``

spec bank_apt::bank {
     spec deposit {
         // pragma aborts_if_is_strict;
         // aborts_if amount == 0;
         // aborts_if !exists<coin::CoinStore<AptosCoin>>(signer::address_of(to));
         // aborts_if global<coin::CoinStore<Coin<AptosCoin>>> (signer::address_of(to)).coin.value < amount ;
         // modifies global<coin::CoinStore<AptosCoin>>(signer::address_of(to));
         // aborts_if global<coin::CoinStore<AptosCoin>>(signer::address_of(to)).coin.value < amount;
    }

    spec withdraw {
        // pragma verify = false;
        // pragma aborts_if_is_partial; // TODO: unable to prove more complex condition 
        // related to transfer of coin
        aborts_if amount == 0;
        aborts_if !exists<Bank>(bank);
        // aborts_if !exists<coin::CoinInfo<coin::CoinStore<AptosCoin>>>(signer::address_of(client));
        aborts_if !coin::spec_is_account_registered<coin::CoinStore<AptosCoin>>(signer::address_of(client));
        aborts_if !coin::is_coin_initialized<coin::CoinStore<AptosCoin>>();
        aborts_if global<coin::CoinStore<AptosCoin>>(signer::address_of(client)).frozen;
        let clients = global<Bank>(bank).clients;
        aborts_if !simple_map::spec_contains_key(clients, signer::address_of(client));
         let client_bank_money = simple_map::spec_get(clients,signer::address_of(client)).value;
        // aborts_if !coin::spec_is_account_registered<coin::CoinStore<AptosCoin>>(signer::address_of(client));
        aborts_if client_bank_money < amount;
         aborts_if global<coin::CoinStore<AptosCoin>>(signer::address_of(client)).coin.value + amount > MAX_U64 ;
        // ensures global<coin::CoinStore<AptosCoin>>(signer::address_of(client)).coin.value == (old(global<coin::CoinStore<AptosCoin>>(signer::address_of(client))).coin.value + amount);
        }
   }

``

Also:

• Reading through the code in the aptos framework repository, I have seen
  that some specifications have the pragma verify=false.
  Does this causes problems when proving stuff?
• I have also seen mentions on the coin.spec
  // TODO(fa_migration)
  Does this means that I need to do things differently?

What error, if any, are you getting?

error file generated by the aptos move prove --dev
prover_error.txt

What have you tried or looked at? Or how can we reproduce the error?

Looked at resources available from the documentation for example:

• Move specification Language here
• Move prover user guide here
• Code in the aptos-framework inside the github repository (for example: coin.spec)

How to reproduce (assuming code here locally available)

inside the directory bank_apt run the prover:

aptos move prove --dev

Which operating system are you using?

Linux (Ubuntu, Fedora, Windows WSL, etc.)

Which SDK or tool are you using? (if any)

Aptos CLI

Describe your environment or tooling in detail

Operating system: Arch Linux (Kernel Linux 6.6.59-1-lts x86_64)
aptos version: aptos 4.3.0
aptos-move-prove 4.3.0

Installed tooling following the guides found in the documentation both for the aptos cli and the prover: no issues found