aptos prover - objects

[MoonShiesty]

Discord user ID

moonshiesty

Describe your question in detail.

im trying to get started with aptos prover, with a module that uses token objects

i thought id start with proving the Object exists after my function creates it:

spec my_module::vault {
    spec create_vault<T: key>(
        owner_addr: address,
        collection_obj: Object<T>
    ): Object<Vault> {
        ensures object::object_exists<Vault>(result.inner);
   }
}

i get these errors:

Error: call to undeclared procedure: $1_aggregator_v2_read_snapshot'u64'\n/ Error: call to undeclared procedure: $1_aggregator_v2_derive_string_concat'u64'\n/

Error: call to undeclared procedure: $1_aggregator_v2_create_derived_string\n10 name resolution errors detected in /boogie.bpl\n"

is it possible to use the prover with token objects?

if not how do i work around this to prove the result after creating a token object

[rahxephon89]

Does this error appear even if you only have this spec? Also, could you try to replace the ensures clause with ensures exists<ObjectCore>(object) && spec_exists_at<T>(object) in your spec and see whether it makes any difference?

[MoonShiesty]

the error actually appears if i run the prover, without any spec files:

➜  mirage-protocol git:(testnet-v2) ✗ aptos move prove --dev 
[INFO] checking specifications
[INFO] rewriting specifications
[INFO] preparing module 0x1004::package_manager
[INFO] preparing module 0x1004::mirage
[INFO] preparing module 0x1004::fee_manager
[INFO] preparing module 0x1004::market
[INFO] preparing module 0x1004::vault
[INFO] transforming bytecode
[INFO] generating verification conditions
[INFO] 270 verification conditions
[INFO] running solver

  "Error": "Move Prover failed: [internal] boogie exited with compilation errors:boogie.bpl(65538,4): Error: call to undeclared procedure: $1_aggregator_v2_read_snapshot'u64'\n/boogie.bpl(67039,4): Error: call to undeclared procedure: $1_aggregator_v2_derive_string_concat'u64'\nboogie.bpl(67057,4): Error: call to undeclared procedure: $1_aggregator_v2_create_derived_string\n3 name resolution errors detected in boogie.bpl\n"
 

do you know why its running 270 verification conditions even though i have zero spec statements in the project?

in a different project i was getting the same error without any spec files and managed to isolate the issue down to a usage of aptos_account::deposit_coins. when i replaced that call with coin::deposit it fixed the issue

tried to replace all the aptos_account::deposit_coins call in this repo and delete any spec files but that didnt completely fix the issue

bit confused how to debug these sorts of issues with the prover, ive just been commenting out lines of code until the prover starts running again. let me know if theres any more info i can provide

[junkil-park]

@MoonShiesty , could you manually apply the change in this PR and run Prover again? The boogie internal errors related to the aggregator v2 native functions should disappear.

[MoonShiesty]

what are the steps to manually apply this change?

[MoonShiesty]

i saw the PR was merged, i did aptos move clean and then ran the dev_scripts from the latest main branch

getting new errors

  "Error": "Move Prover failed: [internal] boogie exited with compilation errors:\nmirage-protocol/boogie.bpl
   (53176,4): Error: mismatched types in assignment command (cannot assign int to bv64)\nmirage-protocol/boogie.bpl
   (84950,9): Error: invalid type for out-parameter 0 in call to $1_timestamp_now_seconds: int
   (expected: bv64)\nmirage-protocol/boogie.bpl(87855,29): Error: invalid type for argument 1 in call to $LeBv64: int
   (expected: bv64)\nmirage-protocol/boogie.bpl(87900,32): Error: invalid type for argument 1 in application of
   $IsEqual'bv64': int (expected: bv64)\nmirage-protocol/boogie.bpl(87926,91): Error: invalid type for argument 1 in
   application of $377f0d7c4aaeea8dd73a7a2c6bc817e59aea569e1f9ae0d2f4a80ea1be93bf01_i64_I64: bv64
   (expected: int)\nmirage-protocol/boogie.bpl(88408,94): Error: invalid type for argument 1 in application of
   $377f0d7c4aaeea8dd73a7a2c6bc817e59aea569e1f9ae0d2f4a80ea1be93bf01_price_Price: bv64
   (expected: int)\nmirage-protocol/boogie.bpl(88408,104): Error: invalid type for argument 3 in application of
   $377f0d7c4aaeea8dd73a7a2c6bc817e59aea569e1f9ae0d2f4a80ea1be93bf01_price_Price: bv64
   (expected: int)\nmirage-protocol/boogie.bpl(88773,98): Error: invalid type for argument 0 in application of
   $377f0d7c4aaeea8dd73a7a2c6bc817e59aea569e1f9ae0d2f4a80ea1be93bf01_price_info_PriceInfo: bv64
   (expected: int)\nmirage-protocol/boogie.bpl(88773,103): Error: invalid type for argument 1 in application of
   $377f0d7c4aaeea8dd73a7a2c6bc817e59aea569e1f9ae0d2f4a80ea1be93bf01_price_info_PriceInfo: bv64
   (expected: int)\nmirage-protocol/boogie.bpl(90881,4): Error: mismatched types in assignment command (cannot assign
   int to bv64)\nmirage-protocol/boogie.bpl(90936,4): Error: mismatched types in assignment command (cannot assign int
   to bv64)\nmirage-protocol/boogie.bpl(91513,4): Error: mismatched types in assignment command (cannot assign bv64 to
   int)\nmirage-protocol/boogie.bpl(92620,9): Error: invalid type for out-parameter 0 in call to
   $1_timestamp_now_seconds: int (expected: bv64)\nmirage-protocol/boogie.bpl(92650,104): Error: invalid type for
   argument 1 in call to $377f0d7c4aaeea8dd73a7a2c6bc817e59aea569e1f9ae0d2f4a80ea1be93bf01_price_info_new: int
   (expected: bv64)\nmirage-protocol/boogie.bpl(92865,9): Error: invalid type for out-parameter 0 in call to
   $1_timestamp_now_seconds: int (expected: bv64)\nmirage-protocol/boogie.bpl(100830,4): Error: mismatched types in
   assignment command (cannot assign int to bv64)\nmirage-protocol/boogie.bpl(103841,9): Error: invalid type for
   out-parameter 0 in call to $4000_rebase_get_elastic: int (expected: bv64)\nmirage-protocol/boogie.bpl
   (114367,4): Error: mismatched types in assignment command (cannot assign bv64 to int)\nmirage-protocol/boogie.bpl
   (114732,4): Error: mismatched types in assignment command (cannot assign bv64 to int)\nmirage-protocol/boogie.bpl
   (116995,4): Error: mismatched types in assignment command (cannot assign bv64 to int)\nmirage-protocol/boogie.bpl
   (117913,4): Error: mismatched types in assignment command (cannot assign bv64 to int)\nmirage-protocol/boogie.bpl
   (176227,53): Error: invalid type for argument 2 in call to $4_property_map_update_typed'u64': bv64
   (expected: int)\nmirage-protocol/boogie.bpl(176282,25): Error: invalid type for argument 0 in application of
   $IsValid'u64': bv64 (expected: int)\nmirage-protocol/boogie.bpl(176340,53): Error: invalid type for argument 2 in
   call to $4_property_map_update_typed'u64': bv64 (expected: int)\nmirage-protocol/boogie.bpl(177159,53): Error:
   invalid type for argument 2 in call to $4_property_map_update_typed'u64': bv64
   (expected: int)\nmirage-protocol/boogie.bpl(177255,53): Error: invalid type for argument 2 in call to
   $4_property_map_update_typed'u64': bv64 (expected: int)\nmirage-protocol/boogie.bpl(177310,25): Error: invalid type
   for argument 0 in application of $IsValid'u64': bv64 (expected: int)\nmirage-protocol/boogie.bpl(177368,53): Error:
   invalid type for argument 2 in call to $4_property_map_update_typed'u64': bv64
   (expected: int)\nmirage-protocol/boogie.bpl(205445,42): Error: invalid type for argument 0 in call to
   $1004_mirage_add_debt: bv64 (expected: int)\nmirage-protocol/boogie.bpl(205569,25): Error: invalid type for argument
   0 in application of $IsValid'u64': bv64 (expected: int)\nmirage-protocol/boogie.bpl(205598,42): Error: invalid type
   for argument 0 in call to $1004_mirage_add_debt: bv64 (expected: int)\nmirage-protocol/boogie.bpl(206014,38): Error:
   invalid type for argument 0 in call to $1_bcs_to_bytes'u64': bv64 (expected: int)\nmirage-protocol/boogie.bpl
   (206031,38): Error: invalid type for argument 0 in call to $1_bcs_to_bytes'u64': bv64
   (expected: int)\nmirage-protocol/boogie.bpl(206929,38): Error: invalid type for argument 0 in call to
   $1_bcs_to_bytes'u64': bv64 (expected: int)\nmirage-protocol/boogie.bpl(206946,38): Error: invalid type for argument
   0 in call to $1_bcs_to_bytes'u64': bv64 (expected: int)\nmirage-protocol/boogie.bpl(207945,38): Error: invalid type
   for argument 0 in call to $1_bcs_to_bytes'u64': bv64 (expected: int)\nmirage-protocol/boogie.bpl(207962,38): Error:
   invalid type for argument 0 in call to $1_bcs_to_bytes'u64': bv64 (expected: int)\n37 type checking errors detected
   in mirage-protocol/boogie.bpl\n"  ```

[rahxephon89]

Also, regarding of the verification condition issue, it is possible that your code relies on some library code, against which some invariants are defined and thus need to be verified.

[MoonShiesty]

i just got started with using the prover yesterday 😅 could you explain what you mean by?

it is possible that your code relies on some library code, against which some invariants are defined and thus need to be verified

i dont have any specs defined in my package but i do rely on library code that doesn't have a spec file such as object tokens/collections

[MoonShiesty]

@junkil-park i tracked some of these issues to:

public fun update_price_feeds {
...
pyth::update_price_feeds(...)
}

was able to workaround with:

    spec update_price_feeds {
        pragma verify = false;
    }

in general, can i workaround these prover issues by turning off verification on the offending functions?

[rahxephon89]

yeah, you could turn them off

[junkil-park]

Taking update_price_feeds as an example, while you're verifying some other functions that are not (related to) update_price_feeds, you can turn the verification off for update_price_feeds to reduce the verification running time and suppress those errors.