[move-prover] better type info scheme

This is the first commit on improving the type reflection modeling in
Move Prover (we expect another commit to complete the overhaul).

In this commit, the type info for a type parameter is modeled as a
Boogie Datatype:

```
var #0_info: $TypeParamInfo;

// where $TypeParamInfo is defined as:

type {:datatype} $TypeParamInfo;

function {:constructor} $TypeParamBool(): $TypeParamInfo;
function {:constructor} $TypeParamU8(): $TypeParamInfo;
function {:constructor} $TypeParamU16(): $TypeParamInfo;
function {:constructor} $TypeParamU32(): $TypeParamInfo;
function {:constructor} $TypeParamU64(): $TypeParamInfo;
function {:constructor} $TypeParamU128(): $TypeParamInfo;
function {:constructor} $TypeParamU256(): $TypeParamInfo;
function {:constructor} $TypeParamAddress(): $TypeParamInfo;
function {:constructor} $TypeParamSigner(): $TypeParamInfo;
function {:constructor} $TypeParamVector(e: $TypeParamInfo): $TypeParamInfo;
function {:constructor} $TypeParamStruct(a: int, m: Vec int, s: Vec int): $TypeParamInfo;
```

This is a more elegant and more expressive encoding than the previous
approach where the type info is modeled by a series of variables:

```
var #0_name: Vec int;
var #0_is_struct: bool;
var #0_account_address: int;
var #0_module_name: Vec int;
var #0_struct_name: Vec int;
```

The second improvement of this commit is the axiomitization of the
relation between a type and its name. This is achieved by defining type
name as an uninterpreted function and using `axiom` to define its
semantics:

```
function $TypeName(t: $TypeParamInfo): Vec int;

axiom is#$TypeParamBool(t) <==> $TypeName(t) == "bool";
axiom is#$TypeParamU8(t) <==> $TypeName(t) == "u8";
axiom is#$TypeParamU16(t) <==> $TypeName(t) == "u16";
axiom is#$TypeParamU32(t) <==> $TypeName(t) == "u32";
axiom is#$TypeParamU64(t) <==> $TypeName(t) == "u64";
axiom is#$TypeParamU128(t) <==> $TypeName(t) == "u128";
axiom is#$TypeParamU256(t) <==> $TypeName(t) == "u256";
axiom is#$TypeParamAddress(t) <==> $TypeName(t) == "address";
axiom is#$TypeParamSigner(t) <==> $TypeName(t) == "signer";

// NOTE: for vector, the axiomization does not parse the vector element name
axiom is#$TypeParamVector(t) ==> $TypeName(t) == "vector<" ++ $TypeName(e#t) ++ ">";
axiom $TypeName(t).starts_with("vector<") && $TypeName(t).ends_with(">") ==> is#$TypeParamVector(t);

// NOTE: for struct, the axiomization does not parse the module and struct name
axiom is#$TypeParamStruct(t) ==> $TypeName(t) == "0x" ++ a#t ++ "::" ++ m#t ++ "::" ++ s#t;
axiom $TypeName(t).starts_with("0x") ==> is#$TypeParamStruct(t);
```

This allows for partial specification of aborts conditions where
`type_info<T>` call is involved (it aborts when `T` is not a struct).
But this is only partial.

The full specification is the work of the next PR, which is to
introduced a `spec fun spec_is_struct<T>(): bool` primitive to capture
this semantics.

language/move-prover/boogie-backend/src/boogie_helpers.rs

@@ -456,9 +456,9 @@ pub fn boogie_debug_track_return(
     boogie_debug_track(fun_target, "$track_return", ret_idx, idx, ty)
 }
 
-enum TypeIdentToken {
+pub enum TypeIdentToken {
     Char(u8),
-    Symbolic(TypeParameterIndex),
+    Variable(String),
 }
 
 impl TypeIdentToken {
@@ -492,18 +492,14 @@ impl TypeIdentToken {
                         k - start,
                         match &tokens[k] {
                             TypeIdentToken::Char(c) => *c,
-                            TypeIdentToken::Symbolic(_) => unreachable!(),
+                            TypeIdentToken::Variable(_) => unreachable!(),
                         }
                     )
                 })
                 .join("");
             format!("Vec(DefaultVecMap(){}, {})", elements, end - start)
         }
 
-        fn get_symbol_name(idx: TypeParameterIndex) -> String {
-            format!("#{}_name", idx)
-        }
-
         // construct all the segments
         let mut segments = vec![];
 
@@ -515,12 +511,12 @@ impl TypeIdentToken {
                         char_seq_start = Some(i);
                     }
                 }
-                TypeIdentToken::Symbolic(idx) => {
+                TypeIdentToken::Variable(name) => {
                     if let Some(start) = &char_seq_start {
                         segments.push(get_char_array(&tokens, *start, i));
                     };
                     char_seq_start = None;
-                    segments.push(get_symbol_name(*idx));
+                    segments.push(name.clone());
                 }
             }
         }
@@ -593,7 +589,10 @@ fn type_name_to_ident_tokens(env: &GlobalEnv, ty: &Type) -> Vec<TypeIdentToken>
             tokens
         }
         Type::TypeParameter(idx) => {
-            vec![TypeIdentToken::Symbolic(*idx)]
+            vec![TypeIdentToken::Variable(format!(
+                "$TypeName(#{}_info)",
+                *idx
+            ))]
         }
         // move types that are not allowed
         Type::Reference(..) | Type::Tuple(..) => {
@@ -679,16 +678,16 @@ fn type_name_to_info_pack(env: &GlobalEnv, ty: &Type) -> Option<TypeInfoPack> {
 /// Convert a type info into a format that can be recognized by Boogie
 pub fn boogie_reflection_type_info(env: &GlobalEnv, ty: &Type) -> (String, String) {
     fn get_symbol_is_struct(idx: TypeParameterIndex) -> String {
-        format!("#{}_is_struct", idx)
+        format!("is#$TypeParamStruct(#{}_info)", idx)
     }
     fn get_symbol_account_address(idx: TypeParameterIndex) -> String {
-        format!("#{}_account_address", idx)
+        format!("a#$TypeParamStruct(#{}_info)", idx)
     }
     fn get_symbol_module_name(idx: TypeParameterIndex) -> String {
-        format!("#{}_module_name", idx)
+        format!("m#$TypeParamStruct(#{}_info)", idx)
     }
     fn get_symbol_struct_name(idx: TypeParameterIndex) -> String {
-        format!("#{}_struct_name", idx)
+        format!("s#$TypeParamStruct(#{}_info)", idx)
     }
 
     let extlib_address = env.get_extlib_address();

language/move-prover/boogie-backend/src/bytecode_translator.rs

@@ -37,7 +37,7 @@ use crate::{
         boogie_modifies_memory_name, boogie_reflection_type_info, boogie_reflection_type_name,
         boogie_resource_memory_name, boogie_struct_name, boogie_temp, boogie_type,
         boogie_type_param, boogie_type_suffix, boogie_type_suffix_for_struct,
-        boogie_well_formed_check, boogie_well_formed_expr,
+        boogie_well_formed_check, boogie_well_formed_expr, TypeIdentToken,
     },
     options::BoogieOptions,
     spec_translator::SpecTranslator,
@@ -91,6 +91,83 @@ impl<'env> BoogieTranslator<'env> {
             writer,
             "\n\n//==================================\n// Begin Translation\n"
         );
+
+        // Add type reflection axioms
+        if !mono_info.type_params.is_empty() {
+            emitln!(writer, "function $TypeName(t: $TypeParamInfo): Vec int;");
+
+            // type name <-> type info: primitives
+            for name in [
+                "Bool", "U8", "U16", "U32", "U64", "U128", "U256", "Address", "Signer",
+            ]
+            .into_iter()
+            {
+                emitln!(
+                    writer,
+                    "axiom (forall t: $TypeParamInfo :: {{$TypeName(t)}} \
+                            is#$TypeParam{}(t) ==> $IsEqual'vec'u8''($TypeName(t), {}));",
+                    name,
+                    TypeIdentToken::convert_to_bytes(TypeIdentToken::make(&name.to_lowercase()))
+                );
+                emitln!(
+                    writer,
+                    "axiom (forall t: $TypeParamInfo :: {{$TypeName(t)}} \
+                            $IsEqual'vec'u8''($TypeName(t), {}) ==> is#$TypeParam{}(t));",
+                    TypeIdentToken::convert_to_bytes(TypeIdentToken::make(&name.to_lowercase())),
+                    name,
+                );
+            }
+
+            // type name <-> type info: vector
+            let mut tokens = TypeIdentToken::make("vector<");
+            tokens.push(TypeIdentToken::Variable(
+                "$TypeName(e#$TypeParamVector(t))".to_string(),
+            ));
+            tokens.extend(TypeIdentToken::make(">"));
+            emitln!(
+                writer,
+                "axiom (forall t: $TypeParamInfo :: {{$TypeName(t)}} \
+                            is#$TypeParamVector(t) ==> $IsEqual'vec'u8''($TypeName(t), {}));",
+                TypeIdentToken::convert_to_bytes(tokens)
+            );
+            // TODO(mengxu): this will parse it to an uninterpreted vector element type
+            emitln!(
+                writer,
+                "axiom (forall t: $TypeParamInfo :: {{$TypeName(t)}} \
+                            ($IsPrefix'vec'u8''($TypeName(t), {}) && $IsSuffix'vec'u8''($TypeName(t), {})) ==> is#$TypeParamVector(t));",
+                TypeIdentToken::convert_to_bytes(TypeIdentToken::make("vector<")),
+                TypeIdentToken::convert_to_bytes(TypeIdentToken::make(">")),
+            );
+
+            // type name <-> type info: struct
+            let mut tokens = TypeIdentToken::make("0x");
+            // TODO(mengxu): this is not a correct radix16 encoding of an integer
+            tokens.push(TypeIdentToken::Variable(
+                "MakeVec1(a#$TypeParamStruct(t))".to_string(),
+            ));
+            tokens.extend(TypeIdentToken::make("::"));
+            tokens.push(TypeIdentToken::Variable(
+                "m#$TypeParamStruct(t)".to_string(),
+            ));
+            tokens.extend(TypeIdentToken::make("::"));
+            tokens.push(TypeIdentToken::Variable(
+                "s#$TypeParamStruct(t)".to_string(),
+            ));
+            emitln!(
+                writer,
+                "axiom (forall t: $TypeParamInfo :: {{$TypeName(t)}} \
+                            is#$TypeParamStruct(t) ==> $IsEqual'vec'u8''($TypeName(t), {}));",
+                TypeIdentToken::convert_to_bytes(tokens)
+            );
+            // TODO(mengxu): this will parse it to an uninterpreted struct
+            emitln!(
+                writer,
+                "axiom (forall t: $TypeParamInfo :: {{$TypeName(t)}} \
+                            $IsPrefix'vec'u8''($TypeName(t), {}) ==> is#$TypeParamVector(t));",
+                TypeIdentToken::convert_to_bytes(TypeIdentToken::make("0x")),
+            );
+        }
+
         // Add given type declarations for type parameters.
         emitln!(writer, "\n\n// Given Types for Type Parameters\n");
         for idx in &mono_info.type_params {
@@ -112,11 +189,7 @@ impl<'env> BoogieTranslator<'env> {
             );
 
             // declare free variables to represent the type info for this type
-            emitln!(writer, "var {}_name: Vec int;", param_type);
-            emitln!(writer, "var {}_is_struct: bool;", param_type);
-            emitln!(writer, "var {}_account_address: int;", param_type);
-            emitln!(writer, "var {}_module_name: Vec int;", param_type);
-            emitln!(writer, "var {}_struct_name: Vec int;", param_type);
+            emitln!(writer, "var {}_info: $TypeParamInfo;", param_type);
         }
         emitln!(writer);
 

language/move-prover/boogie-backend/src/prelude/native.bpl

@@ -22,6 +22,18 @@ function $IsEqual'vec{{S}}'(v1: Vec ({{T}}), v2: Vec ({{T}})): bool {
 }
 {%- endif %}
 
+// Not inlined.
+function $IsPrefix'vec{{S}}'(v: Vec ({{T}}), prefix: Vec ({{T}})): bool {
+    LenVec(v) >= LenVec(prefix) &&
+    (forall i: int:: InRangeVec(prefix, i) ==> $IsEqual{{S}}(ReadVec(v, i), ReadVec(prefix, i)))
+}
+
+// Not inlined.
+function $IsSuffix'vec{{S}}'(v: Vec ({{T}}), suffix: Vec ({{T}})): bool {
+    LenVec(v) >= LenVec(suffix) &&
+    (forall i: int:: InRangeVec(suffix, i) ==> $IsEqual{{S}}(ReadVec(v, LenVec(v) - LenVec(suffix) + i), ReadVec(suffix, i)))
+}
+
 // Not inlined.
 function $IsValid'vec{{S}}'(v: Vec ({{T}})): bool {
     $IsValid'u64'(LenVec(v)) &&

language/move-prover/boogie-backend/src/prelude/prelude.bpl

@@ -1024,3 +1024,20 @@ axiom $EventStore__is_empty($EmptyEventStore);
 procedure {:inline 1} $InitEventStore() {
 }
 {%- endif %}
+
+// ============================================================================================
+// Type Reflection on Type Parameters
+
+type {:datatype} $TypeParamInfo;
+
+function {:constructor} $TypeParamBool(): $TypeParamInfo;
+function {:constructor} $TypeParamU8(): $TypeParamInfo;
+function {:constructor} $TypeParamU16(): $TypeParamInfo;
+function {:constructor} $TypeParamU32(): $TypeParamInfo;
+function {:constructor} $TypeParamU64(): $TypeParamInfo;
+function {:constructor} $TypeParamU128(): $TypeParamInfo;
+function {:constructor} $TypeParamU256(): $TypeParamInfo;
+function {:constructor} $TypeParamAddress(): $TypeParamInfo;
+function {:constructor} $TypeParamSigner(): $TypeParamInfo;
+function {:constructor} $TypeParamVector(e: $TypeParamInfo): $TypeParamInfo;
+function {:constructor} $TypeParamStruct(a: int, m: Vec int, s: Vec int): $TypeParamInfo;

language/move-prover/tests/sources/functional/type_reflection.move

@@ -99,4 +99,15 @@ module 0x42::test {
         // this should not pass
         aborts_if false;
     }
+
+    fun test_type_info_can_abort_if<T>(): (type_info::TypeInfo, string::String) {
+        (type_info::type_of<T>(), type_info::type_name<T>())
+    }
+    spec test_type_info_can_abort_if {
+        pragma aborts_if_is_partial = true;
+        aborts_if type_info::type_name<T>().bytes == b"bool";
+        aborts_if type_info::type_name<T>().bytes == b"u64";
+        aborts_if type_info::type_name<T>().bytes == b"signer";
+        aborts_if type_info::type_name<T>().bytes == b"vector<address>";
+    }
 }