aptos move prover - proving Object<T>(addr) exists_at<T>(addr) after move_to(addr, T{...})

[MoonShiesty]

Discord user ID

moonshiesty

Describe your question in detail.

currently it looks like its not possible to specify that an object::exists_at<T>(addr) after move_to(addr, T{...})

the issue im facing is i have a function that creates and returns an Object<T>, ie

fun create(seeds: vector<u8>): Object<MyType> {
              let constructor_ref = object::create_named_object(&package_manager::get_signer(), seeds)}
               move_to<MyType>(&oracle_signer, MyType{...};
               object::address_to_object<MyType>(address_from_constructor_ref(&constructor_ref))
}

i can't prove that the function doesn't abort with

194 │         assert!(exists_at<T>(object), error::not_found(ERESOURCE_DOES_NOT_EXIST));
    │         ------------------------------------------------------------------------- abort happened here with code 0x6

since converting the address to object require that the type object::exists_at the address, and exists_at is native and unspecified. therefore the prover doesn't know that MyType exists at the constructor reference

since it looks the native impl ofobject::exists_at(obj_addr) only differs from exists<T>(obj_addr) in gas cost, and aborts in the same cases im thinking i can solve this issue by opening a PR in aptos-core to add this specification to spec_exists_at:

    spec exists_at<T: key>(object: address): bool {
        ensures [abstract] result == exists<T>(object);
    }

why does aptos need a native exists and object::exists_at and would this additional specification for object::exists_at be sound?

i tried to add that line to object.spec.move but the prover failed with:

thread 'tokio-runtime-worker' panicked at third_party/move/move-model/src/ty.rs:1019:13:
expected `Type::Struct`, found: `TypeParameter(0)`
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

[MoonShiesty]

i can get this example to work if i add the following incorrect spec:

        let object_address = object::spec_create_object_address(@package_address, seeds);
        aborts_if !object::spec_exists_at<Oracle>(object_addr);

when function would abort at runtime if the object that it creates already exists_at the address

[rahxephon89]

Hi @MoonShiesty, object is not well supported by the prover currently. More specifically, we cannot specify like you suggested:

    spec exists_at<T: key>(object: address): bool {
        ensures [abstract] result == exists<T>(object);
    }

We have an issue to track this: aptos-labs/aptos-core#6658 and will hopefully fix this in the near future.

[MoonShiesty]

interesting thread

seems like this could become easier to fix once aptos supports returning global references

aptos-labs/aptos-core#6777 (comment)

more generally, can spec functions work with global references once compiler v2 supports returning global references?

[rahxephon89]

yeah, that is an interesting direction we would like to explore.