Need Help for Writing a Specification

[seyyedaliayati]

❓ Questions and Help

Please note that this issue tracker is not a help form and this issue will be closed.

Please contact the development team on Discord

Consider the following function from wormhole smart contract:

        let to_chain = transfer::get_to_chain(transfer);
        assert!(to_chain == wormhole::state::get_chain_id(), E_INVALID_TARGET);
        let token_chain = transfer::get_token_chain(transfer);
        let token_address = transfer::get_token_address(transfer);
        let origin_info = state::create_origin_info(token_chain, token_address);

        state::assert_coin_origin_info<CoinType>(origin_info);

        let decimals = coin::decimals<CoinType>();

        let amount = normalized_amount::denormalize(transfer::get_amount(transfer), decimals);
        let fee_amount = normalized_amount::denormalize(transfer::get_fee(transfer), decimals);

        let recipient = from_bcs::to_address(get_bytes(&transfer::get_to(transfer)));

        let recipient_coins: Coin<CoinType>;

        if (state::is_wrapped_asset<CoinType>()) {
            recipient_coins = wrapped::mint<CoinType>(amount);
        } else {
            let token_bridge = state::token_bridge_signer();
            recipient_coins = coin::withdraw<CoinType>(&token_bridge, amount);
        };

        // take out fee from the recipient's coins. `extract` will revert
        // if fee > amount
        let fee_coins = coin::extract(&mut recipient_coins, fee_amount);
        coin::deposit(recipient, recipient_coins);
        coin::deposit(fee_recipient, fee_coins);
    }```

I want to write a specification to verify this function. I wrote than the following spec but it fails:

spec complete_transfer(transfer: &Transfer, fee_recipient: address) { let post val = global<CoinStore>(fee_recipient).coin.value; ensures val == transfer.fee.amount + old(global<CoinStore>(fee_recipient).coin.value); }```

Can someone help fee to find out what's happening??