Skip to content
This repository has been archived by the owner on May 4, 2024. It is now read-only.

[move-prover] model type_of which returns the struct tag triple #462

Merged
merged 1 commit into from
Sep 8, 2022

Conversation

meng-xu-cs
Copy link
Collaborator

The type_of primitive is another type reflection feature supported by the move prover:

At its core, the type_of function returns information about a user-defined struct type:

struct TypeInfo has copy, drop, store {
    account_address: address,
    module_name: vector<u8>,
    struct_name: vector<u8>,
}

public native fun type_of<T>: TypeInfo;

This is similar to the type_name feature with the following complication:

  • type_of<T> will panic if T is not a user-defined struct type. type_of<vector<bool>> will cause the Move VM to abort. This needs to be captured by the prover as well. On the other hand, type_name will never panic and will always return a canonical representation of the passed in type tag.
  • type_of<T> does not care about the type arguments of the struct type. E.g., if there is a struct Foo<K, V>, then both type_of<Foo<bool, int>> and type_of<Foo<int, bool>> will return exactly the same information.

With that said, type_of is handled in a similar way to type_name:

  • If the type argument T is statically known, all fields of the TypeInfo struct will be pre-determined as constants. However, there is a caveat when T is not a user-defined type in spec function context.
  • If the type argument T is symbolic in the verification context, we rely on the following newly introduced fresh variables to model the information of T, including
    • #T_is_struct: bool; to model whether T is a user-defined struct
    • #T_account_address: int;
    • #T_module_name: Vec int;
    • #T_struct_name: Vec int;, for these variables, the name says all

In the bytecode context (i.e., Move function context), a type_of<T> function call is translated as:

if (!<predicate_is_struct>) {
    call $ExecFailureAbort();
} else {
    retval := <struct_info_variable>;
}

In this way, we still capture the fact that type_of<T>() may abort when T is not a struct type.

However, in spec function context, due to the fact that a spec function is essentially an expression. The rewriting mechanism does not allow us (or at least it is not easy) to instrument an additional check that T must be a struct type. In light of this, the <is_struct> flag is ignored and we assume T passed in is a struct.

Motivation

Support type reflection

Have you read the Contributing Guidelines on pull requests?

Yes

Test Plan

  • CI
  • New test case added

The `type_of` primitive is another type reflection feature supported by
the move prover:

At its core, the `type_of` function returns information about a
user-defined struct type:

```move
struct TypeInfo has copy, drop, store {
    account_address: address,
    module_name: vector<u8>,
    struct_name: vector<u8>,
}

public native fun type_of<T>: TypeInfo;
```

This is similar to the `type_name` feature with the following
complication:
- `type_of<T>` will panic if `T` is not a user-defined struct type.
  `type_of<vector<bool>>` will cause the Move VM to abort. This needs to
  be captured by the prover as well. On the other hand, `type_name` will
  never panic and will always return a canonical representation of the
  passed in type tag.
- `type_of<T>` does not care about the type arguments of the struct
  type. E.g., if there is a struct `Foo<K, V>`, then both
  `type_of<Foo<bool, int>>` and `type_of<Foo<int, bool>>` will return
  exactly the same information.

With that said, `type_of` is handled in a similar way to `type_name`:

- If the type argument `T` is statically known, all fields of the
  `TypeInfo` struct will be pre-determined as constants. However, there
  is a caveat when `T` is not a user-defined type in spec function
  context.
- If the type argument `T` is symbolic in the verification context, we
  rely on the following newly introduced fresh variables to model the
  information of `T`, including
  - `#T_is_struct: bool;` to model whether `T` is a user-defined struct
  - `#T_account_address: int;`
  - `#T_module_name: Vec int;`
  - `#T_struct_name: Vec int;`, for these variables, the name says all

In the bytecode context (i.e., Move function context), a `type_of<T>`
function call is translated as:

```
if (!<predicate_is_struct>) {
    call $ExecFailureAbort();
} else {
    retval := <struct_info_variable>;
}
```

In this way, we still capture the fact that `type_of<T>()` may abort
when `T` is not a struct type.

However, in spec function context, due to the fact that a spec function
is essentially an expression. The rewriting mechanism does not allow us
(or at least it is not easy) to instrument an additional check that `T`
must be a struct type. In light of this, the `<is_struct>` flag is
ignored and we assume `T` passed in is a struct.
@jolestar
Copy link
Collaborator

jolestar commented Sep 8, 2022

It is possible to get the TypeInfo through a built-in function instead of the native function?
Because the Move modules bytecode contains the type info.
Of course, the generic type is a problem.

@meng-xu-cs
Copy link
Collaborator Author

It is possible to get the TypeInfo through a built-in function instead of the native function?

I am not entirely sure that I understand the question. Here are some interpretations I can guess and I'll try to answer them:

  • "built-in" function vs "native" function.
    This is the part that confuses me. I don't think we have a distinction between built-in and native function? If the question is,
    • why don't we have a bytecode that corresponds to getting the type info instead of a native function...
      well, that is a large topic to debate. But based on how similar features are implemented in other languages (Rust, Python), I think the native function is the common practice.
    • why don't we have the type_of function in move-stdlib?
      I am definitely not the best contact for this question but it is generally preferable to keep a stdlib small and with mature features only.

Also I would like to point out that this is the verification support for type reflection. To get runtime support, the native function implementation needs to be supplied to the Move VM, similar to how other native functions are plugged-in in the stdlib.

the generic type is a problem.

Yes. Generic type is only a problem in the verification context (i.e., to Move Prover). In the concrete execution context (i.e., to Move VM), the generic type parameter will be resolved to some concrete type at runtime.

@wrwg
Copy link
Member

wrwg commented Sep 8, 2022

It is possible to get the TypeInfo through a built-in function instead of the native function?

I am not entirely sure that I understand the question. Here are some interpretations I can guess and I'll try to answer them:

  • "built-in" function vs "native" function.
    This is the part that confuses me. I don't think we have a distinction between built-in and native function? If the question is,

    • why don't we have a bytecode that corresponds to getting the type info instead of a native function...
      well, that is a large topic to debate. But based on how similar features are implemented in other languages (Rust, Python), I think the native function is the common practice.
    • why don't we have the type_of function in move-stdlib?
      I am definitely not the best contact for this question but it is generally preferable to keep a stdlib small and with mature features only.

Also I would like to point out that this is the verification support for type reflection. To get runtime support, the native function implementation needs to be supplied to the Move VM, similar to how other native functions are plugged-in in the stdlib.

the generic type is a problem.

Yes. Generic type is only a problem in the verification context (i.e., to Move Prover). In the concrete execution context (i.e., to Move VM), the generic type parameter will be resolved to some concrete type at runtime.

It does not really make sense for us in this context to discuss the design of features like type_name or type_info. These are pre-given designs and we are reflecting them with our specification/verification tech. This PR is about doing this for the Move prover, and I think this goes into the right direction, hence approving.

@meng-xu-cs meng-xu-cs merged commit f57c130 into move-language:main Sep 8, 2022
@jolestar
Copy link
Collaborator

jolestar commented Sep 8, 2022

  • "built-in" function vs "native" function.
    This is the part that confuses me. I don't think we have a distinction between built-in and native function? If the question is,

built-in function needs a bytecode like borrow_global, it implements in the compiler and VM.
native function needs binding the rust implement with Move function when init VM.

Of course, this PR is about Move prover, we can discuss this feature when introduce it in move-stdlib.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants