This solves a very Sui-specific problem and, as such, is unlikely to to be cherry-picked to the main branch. The problem is that in Sui we need to implement a native function in Boogie that allows us to retrieve an UID of an object of arbitrary (object type). The only way to do it is to encode it directly in Boogie as it needs to work for generic types and while in Sui we maintain the invariant that a Move struct with a key ability will ALWAYS have the first field of type sui::object::UID, the Move language itself (particularly its type system) is unaware of this making the following piece of code illegal:
fun foo<T: key>(o: T): UID {
o.id
}
Instead, in these types of cases we use a native function to retrieve a UID of an object that in Boogie looks as follows:
function $2_object_$borrow_uid{{S}}(obj: {{T}}): $2_object_UID {
$id#{{T}}(obj)
}
Unfortunately, T and S in the above code can be expanded to types representing type paremeters (#t1, #t2, etc.) whose definitions are injected during bytecode translation process to represent type parameters that cannot be resolved.
In Sui, this is a problem, as it makes the expanded version of $id#{{T}}(obj) illegal (and causing a build failure) due to, by default, the Boogie definition of type parameters not having the id field. This PR adds this field to the respective types while they are generated to satisfy the Boogie compiler.
The idea for this solution has been proposed by @emmazzz - great thanks!
Motivation
This solves a very Sui-specific problem and, as such, is unlikely to to be cherry-picked to the main branch. The problem is that in Sui we need to implement a native function in Boogie that allows us to retrieve an UID of an object of arbitrary (object type). The only way to do it is to encode it directly in Boogie as it needs to work for generic types and while in Sui we maintain the invariant that a Move struct with a
keyability will ALWAYS have the first field of typesui::object::UID, the Move language itself (particularly its type system) is unaware of this making the following piece of code illegal:Instead, in these types of cases we use a native function to retrieve a UID of an object that in Boogie looks as follows:
Unfortunately,
TandSin the above code can be expanded to types representing type paremeters (#t1,#t2, etc.) whose definitions are injected during bytecode translation process to represent type parameters that cannot be resolved.In Sui, this is a problem, as it makes the expanded version of
$id#{{T}}(obj)illegal (and causing a build failure) due to, by default, the Boogie definition of type parameters not having theidfield. This PR adds this field to the respective types while they are generated to satisfy the Boogie compiler.The idea for this solution has been proposed by @emmazzz - great thanks!
Have you read the Contributing Guidelines on pull requests?
Yes