[Prover] the use of a type parameter with exists in spec

[junkil-park]

How to reproduce

This case is from the object module in the aptos_framework. To reproduce, run Prover uncommenting the ensures line.

    native fun exists_at<T: key>(object: address): bool;
    spec exists_at {
        pragma opaque;
        aborts_if false;
        // TODO: Disabled the following post-condition due to an issue with
        // the use of a type parameter in `exists` in spec.
        // ensures result == exists<T>(object);
    }

The current version of Prover fails during the model building process, complaining that:

error: The type argument to `exists` and `global` must be a struct type but #0 is not a struct type.
  ┌─ ./sources/object.spec.move:7:27
  │
7 │         ensures result == exists<T>(object);
  │                           ^^^^^^^^^^^^^^^^^

Error: exiting with model building errors

Expected output

Prover runs without an error.

[github-actions]

This issue is stale because it has been open 45 days with no activity. Remove the stale label or comment - otherwise this will be closed in 15 days.

[rahxephon89]

Close since #6777 resolved it.

[rahxephon89]

Reopen this to track the feature request to support exists_at in the spec.

[wrwg]

Why do we need exists_at at spec level? One can just use exists in specifications, since specs do not have the restriction to only do this for resources in the same module.

[rahxephon89]

Why do we need exists_at at spec level? One can just use exists in specifications, since specs do not have the restriction to only do this for resources in the same module.

When exists_at is instantiated with a concrete type, it is OK to use exists. But in the function public fun address_to_object<T: key>(object: address): Object<T> in the object module, exists_at is used in the assert statement and generic types such as exists<T> are not supported in the spec language.

[wrwg]

Why do we need exists_at at spec level? One can just use exists in specifications, since specs do not have the restriction to only do this for resources in the same module.

When exists_at is instantiated with a concrete type, it is OK to use exists. But in the function public fun address_to_object<T: key>(object: address): Object<T> in the object module, exists_at is used in the assert statement and generic types such as exists<T> are not supported in the spec language.

Then we probably should fix the bug that generic types are not supported for exists?