Move prove failure for the swap function

[sepine]

Hi, I am a new developer for aptos and move.

I am trying to write some spec to formally verify whether the swap function can meet the stable curve x^3y+xy^3=k.

However, when I write the following spec for this curve

spec swap {
        // pre
        requires !emergency::is_emergency();
        requires exists<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account);
        // requires !borrow_global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).locked;

        requires !global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).locked;
        requires x_in.value > 0 && y_in.value > 0;
        ensures 
            (
                global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_x_reserve.value * 
                global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_x_reserve.value * 
                global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_x_reserve.value * 
                global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_y_reserve.value
            ) + 
            (
                global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_x_reserve.value * 
                global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_y_reserve.value * 
                global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_y_reserve.value * 
                global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_y_reserve.value
            )
            >=     
            (
                old(global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_x_reserve.value) * 
                old(global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_x_reserve.value) * 
                old(global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_x_reserve.value) * 
                old(global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_y_reserve.value)
            ) + 
            (
                old(global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_x_reserve.value) * 
                old(global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_y_reserve.value) * 
                old(global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_y_reserve.value) * 
                old(global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_y_reserve.value)
            );

I got the following error post-condition does not hold

error: post-condition does not hold
┌─ /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.spec.move:76:9
│
76 │ ╭ ensures
77 │ │ (
78 │ │ global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_x_reserve.value *
79 │ │ global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_x_reserve.value *
· │
100 │ │ old(global<LiquidityPool<X, Y, Curve>>(@liquidswap_pool_account).coin_y_reserve.value)
101 │ │ );
│ ╰──────────────^
│
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.move:294: swap
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.spec.move:42
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.spec.move:43
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.spec.move:46
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.spec.move:47
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.move:294: swap
= x_in = coin.Coin{value = 1258}
= x_out = 1262
= y_in = coin.Coin{value = 763}
= y_out = 754
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.move:300: swap
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/emergency.move:73: assert_no_emergency
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/emergency.move:68: is_emergency
= result = false
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/emergency.move:69: is_emergency
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/emergency.move:73: assert_no_emergency
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/emergency.move:74: assert_no_emergency
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.move:302: swap
= at /media/user/xxx/move/move_projects/liquidswap/sources/libs/coin_helper.move:59: is_sorted
= at /media/user/xxx/move/move_projects/liquidswap/sources/libs/coin_helper.move:33: compare
= x_info =
= type_info.TypeInfo{
= account_address = 0x33f,
= module_name = vector{(size): 832, default: 101u8},
= struct_name =
= vector{
= (size): 18446744073709551614,
= <? Literal("257")>,
= 2: <? Literal("836")>,
= default: 101u8}}
= at /media/user/xxx/move/move_projects/liquidswap/sources/libs/coin_helper.move:34: compare
= y_info =
= type_info.TypeInfo{
= account_address = 0x33c,
= module_name = vector{(size): 829, default: 101u8},
= struct_name =
= vector{
= (size): 18446744073709551614,
= <? Literal("258")>,
= 2: <? Literal("835")>,
= default: 101u8}}
= at /media/user/xxx/move/move_projects/liquidswap/sources/libs/coin_helper.move:37: compare
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/type_info.move:34: chain_id_internal
= self =
= type_info.TypeInfo{
= account_address = 0x33f,
= module_name = vector{(size): 832, default: 101u8},
= struct_name =
= vector{
= (size): 18446744073709551614,
= <? Literal("257")>,
= 2: <? Literal("836")>,
= default: 101u8}}
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/type_info.move:35: struct_name
= result =
= vector{
= (size): 18446744073709551614,
= <? Literal("257")>,
= 2: <? Literal("836")>,
= default: 101u8}
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/type_info.move:36: struct_name
= x_struct_name =
= vector{
= (size): 18446744073709551614,
= <? Literal("257")>,
= 2: <? Literal("836")>,
= default: 101u8}
= at /media/user/xxx/move/move_projects/liquidswap/sources/libs/coin_helper.move:38: compare
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/type_info.move:34: chain_id_internal
= self =
= type_info.TypeInfo{
= account_address = 0x33c,
= module_name = vector{(size): 829, default: 101u8},
= struct_name =
= vector{
= (size): 18446744073709551614,
= <? Literal("258")>,
= 2: <? Literal("835")>,
= default: 101u8}}
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/type_info.move:35: struct_name
= result =
= vector{
= (size): 18446744073709551614,
= <? Literal("258")>,
= 2: <? Literal("835")>,
= default: 101u8}
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/type_info.move:36: struct_name
= y_struct_name =
= vector{
= (size): 18446744073709551614,
= <? Literal("258")>,
= 2: <? Literal("835")>,
= default: 101u8}
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.spec.move:25
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.spec.move:26
= at /media/user/xxx/move/move_projects/liquidswap/sources/libs/coin_helper.move:39: compare
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.spec.move:25
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.spec.move:26
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.move:30: compare
= left =
= right =
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.move:31: compare
= left_bytes = vector{(size): 1, default: 101u8}
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.move:32: compare
= right_bytes = vector{(size): 2, default: 101u8}
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.spec.move:37
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.spec.move:38
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.move:34: compare
= result = comparator.Result{inner = 1u8}
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.move:35: compare
= struct_cmp = comparator.Result{inner = 1u8}
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.spec.move:8
= at /media/user/xxx/move/move_projects/liquidswap/sources/libs/coin_helper.move:40: compare
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.spec.move:8
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.move:14: is_equal
= self = comparator.Result{inner = 1u8}
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.move:15: is_equal
= result = false
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.move:16: is_equal
= at /media/user/xxx/move/move_projects/liquidswap/sources/libs/coin_helper.move:40: compare
= result = comparator.Result{inner = 1u8}
= at /media/user/xxx/move/move_projects/liquidswap/sources/libs/coin_helper.move:54: compare
= order = comparator.Result{inner = 1u8}
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.spec.move:8
= at /media/user/xxx/move/move_projects/liquidswap/sources/libs/coin_helper.move:60: is_sorted
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.spec.move:8
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.move:14: is_equal
= self = comparator.Result{inner = 1u8}
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.move:15: is_equal
= result = false
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.move:16: is_equal
= at /media/user/xxx/move/move_projects/liquidswap/sources/libs/coin_helper.move:60: is_sorted
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.spec.move:14
= at /media/user/xxx/move/move_projects/liquidswap/sources/libs/coin_helper.move:61: is_sorted
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.spec.move:14
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.move:18: is_smaller_than
= self = comparator.Result{inner = 1u8}
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.move:19: is_smaller_than
= result = true
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/../aptos-stdlib/sources/comparator.move:20: is_smaller_than
= result = true
= at /media/user/xxx/move/move_projects/liquidswap/sources/libs/coin_helper.move:62: is_sorted
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.move:302: swap
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.move:303: swap
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.move:305: swap
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.move:609: assert_pool_unlocked
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.move:610: assert_pool_unlocked
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.move:611: assert_pool_unlocked
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.move:307: swap
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/sources/coin.move:1160: value
= coin = coin.Coin{value = 1258}
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/sources/coin.move:1161: value
= result = 1258
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/sources/coin.move:1162: value
= x_in_val = 1258
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.move:308: swap
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/sources/coin.move:1160: value
= coin = <? List([Literal("|$1_coin_Coin'#1'|"), Literal("763")])>
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/sources/coin.move:1161: value
= result = 763
= at /home/xxx/.move/https___github_com_aptos-labs_aptos-core_git_mainnet/aptos-move/framework/aptos-framework/sources/coin.move:1162: value
= y_in_val = 763
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.move:310: swap
= at /media/user/xxx/move/move_projects/liquidswap/sources/swap/liquidity_pool.move:312: swap
= pool =
= &liquidity_pool.LiquidityPool{
= coin_x_reserve = coin.Coin{value = 6},
= coin_y_reserve = coin.Coin{value = 1},
= last_block_timestamp = 0,
= last_price_x_cumulative = 0u128,
= last_price_y_cumulative = 0u128,
= lp_mint_cap = coin.MintCapability{dummy_field = false},
= lp_burn_cap = coin.BurnCapability{dummy_field = false},
= x_scale = 0,
= y_scale = 0,
= locked = false,
= fee = 2,
= dao_fee = 800}
................. too long ...........
{
"Error": "Move Prover failed: exiting with verification errors"
}

Thanks.