-
Notifications
You must be signed in to change notification settings - Fork 685
[move-prover] model type_of
which returns the struct tag triple
#462
Conversation
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.
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:
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.
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 |
Of course, this PR is about Move prover, we can discuss this feature when introduce it in move-stdlib. |
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:This is similar to the
type_name
feature with the following complication:type_of<T>
will panic ifT
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 structFoo<K, V>
, then bothtype_of<Foo<bool, int>>
andtype_of<Foo<int, bool>>
will return exactly the same information.With that said,
type_of
is handled in a similar way totype_name
:T
is statically known, all fields of theTypeInfo
struct will be pre-determined as constants. However, there is a caveat whenT
is not a user-defined type in spec function context.T
is symbolic in the verification context, we rely on the following newly introduced fresh variables to model the information ofT
, including#T_is_struct: bool;
to model whetherT
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 allIn the bytecode context (i.e., Move function context), a
type_of<T>
function call is translated as:In this way, we still capture the fact that
type_of<T>()
may abort whenT
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 assumeT
passed in is a struct.Motivation
Support type reflection
Have you read the Contributing Guidelines on pull requests?
Yes
Test Plan