Dynamic field UID Fix

crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs

@@ -388,6 +388,30 @@ impl<'env> BoogieTranslator<'env> {
         }
 
         // Add given type declarations for type parameters.
+        // Collect type param indices that appear in UID's dynamic field entries.
+        // These cannot be declared as datatypes containing UID (would create a cycle).
+        let uid_df_type_params: BTreeSet<u16> = env
+            .uid_qid()
+            .map(|uid_qid| {
+                let uid_type = Type::Datatype(uid_qid.module_id, uid_qid.id, vec![]);
+                let df_info = dynamic_field_analysis::get_env_info(env);
+                let mut params = BTreeSet::new();
+                for (name, value) in df_info.dynamic_field_names_values(&uid_type) {
+                    name.visit(&mut |t| {
+                        if let Type::TypeParameter(idx) = t {
+                            params.insert(*idx);
+                        }
+                    });
+                    value.visit(&mut |t| {
+                        if let Type::TypeParameter(idx) = t {
+                            params.insert(*idx);
+                        }
+                    });
+                }
+                params
+            })
+            .unwrap_or_default();
+
         emitln!(writer, "\n\n// Given Types for Type Parameters\n");
         for idx in &mono_info.type_params {
             let param_type = boogie_type_param(env, *idx);
@@ -397,9 +421,10 @@ impl<'env> BoogieTranslator<'env> {
                 .find_datatype_by_tag(&StructTag::from_str("0x2::object::UID").unwrap())
                 .and_then(|uid_qid| mono_info.structs.get(&uid_qid))
                 .is_some();
-            if is_uid {
+            if is_uid && !uid_df_type_params.contains(idx) {
                 // Sui-specific to allow "using" unresolved type params as Sui objects in Boogie
-                // (otherwise Boogie compilation errors may occur)
+                // (otherwise Boogie compilation errors may occur).
+                // Skip if this type param appears in UID's dynamic fields to avoid circularity.
                 emitln!(writer, "datatype {} {{", param_type);
                 emitln!(writer, "    {}($id: $2_object_UID)", param_type);
                 emitln!(writer, "}");
@@ -467,6 +492,7 @@ impl<'env> BoogieTranslator<'env> {
                             self.env,
                             self.targets,
                             &struct_env.get_qualified_id(),
+                            type_inst,
                         ),
                     }
                     .translate();
@@ -491,6 +517,7 @@ impl<'env> BoogieTranslator<'env> {
                             self.env,
                             self.targets,
                             &enum_env.get_qualified_id(),
+                            type_inst,
                         ),
                     }
                     .translate();
@@ -1436,10 +1463,16 @@ impl<'env> StructTranslator<'env> {
             )
         });
         let dynamic_fields = dynamic_field_names_values.iter().map(|(name, value)| {
+            let value_type = boogie_type(env, value);
+            let value_type = if value_type.contains(' ') {
+                format!("({})", value_type)
+            } else {
+                value_type
+            };
             format!(
                 "{}: (Table int {})",
                 boogie_dynamic_field_sel(self.parent.env, name, value),
-                boogie_type(env, value),
+                value_type,
             )
         });
         let all_fields = fields.chain(dynamic_fields).join(", ");
@@ -1486,12 +1519,18 @@ impl<'env> StructTranslator<'env> {
             );
         }
         for (pos, (name, value)) in dynamic_field_names_values.iter().enumerate() {
+            let value_type = boogie_type(env, value);
+            let value_type = if value_type.contains(' ') {
+                format!("({})", value_type)
+            } else {
+                value_type
+            };
             self.emit_function(
                 &format!(
                     "{}(s: {}, x: (Table int {})): {}",
                     boogie_dynamic_field_update(struct_env, self.type_inst, name, value),
                     struct_name,
-                    boogie_type(env, value),
+                    value_type,
                     struct_name
                 ),
                 || {

crates/move-prover-boogie-backend/src/boogie_backend/lib.rs

@@ -230,12 +230,12 @@ pub fn add_prelude(
         .collect_vec();
     let mut table_instances = vec![];
     if let Some(table_qid) = env.table_qid() {
-        if mono_info.is_used_datatype(env, targets, &table_qid) {
+        if mono_info.is_used_datatype(env, targets, &table_qid, &[]) {
             table_instances.push(TableImpl::table(env, options, &mono_info, table_qid, false));
         }
     }
     if let Some(object_table_qid) = env.object_table_qid() {
-        if mono_info.is_used_datatype(env, targets, &object_table_qid) {
+        if mono_info.is_used_datatype(env, targets, &object_table_qid, &[]) {
             table_instances.push(TableImpl::object_table(
                 env,
                 options,
@@ -249,11 +249,13 @@ pub fn add_prelude(
     let uid_qid = env.uid_qid();
     for info in dynamic_field_analysis::get_env_info(env).dynamic_fields() {
         let (struct_qid, type_inst) = info.0.get_datatype().unwrap();
-        if mono_info.is_used_datatype(env, targets, &struct_qid)
-            && mono_info
-                .structs
-                .get(&struct_qid)
-                .is_some_and(|type_inst_set| type_inst_set.contains(type_inst))
+        let is_uid_type = uid_qid.as_ref().is_some_and(|uid| *uid == struct_qid);
+        if is_uid_type
+            || (mono_info.is_used_datatype(env, targets, &struct_qid, &[])
+                && mono_info
+                    .structs
+                    .get(&struct_qid)
+                    .is_some_and(|type_inst_set| type_inst_set.contains(type_inst)))
         {
             dynamic_field_instances.push(DynamicFieldInfo::dynamic_field(
                 env, options, info.0, info.1, false,
@@ -305,7 +307,7 @@ pub fn add_prelude(
             .find_struct(env.symbol_pool().make("Option"))
             .unwrap();
         let option_instances =
-            if mono_info.is_used_datatype(env, targets, &option_env.get_qualified_id()) {
+            if mono_info.is_used_datatype(env, targets, &option_env.get_qualified_id(), &[]) {
                 mono_info
                     .structs
                     .get(&option_env.get_qualified_id())
@@ -323,42 +325,50 @@ pub fn add_prelude(
         let vec_set_struct_env = vec_set_module_env
             .find_struct(env.symbol_pool().make("VecSet"))
             .unwrap();
-        let vec_set_instances =
-            if mono_info.is_used_datatype(env, targets, &vec_set_struct_env.get_qualified_id()) {
-                mono_info
-                    .structs
-                    .get(&vec_set_struct_env.get_qualified_id())
-                    .unwrap_or(&BTreeSet::new())
-                    .iter()
-                    .map(|tys| TypeInfo::new(env, options, &tys[0], false))
-                    .collect_vec()
-            } else {
-                vec![]
-            };
+        let vec_set_instances = if mono_info.is_used_datatype(
+            env,
+            targets,
+            &vec_set_struct_env.get_qualified_id(),
+            &[],
+        ) {
+            mono_info
+                .structs
+                .get(&vec_set_struct_env.get_qualified_id())
+                .unwrap_or(&BTreeSet::new())
+                .iter()
+                .map(|tys| TypeInfo::new(env, options, &tys[0], false))
+                .collect_vec()
+        } else {
+            vec![]
+        };
         context.insert("vec_set_instances", &vec_set_instances);
     }
 
     if let Some(vec_map_module_env) = env.find_module_by_name(env.symbol_pool().make("vec_map")) {
         let vec_map_struct_env = vec_map_module_env
             .find_struct(env.symbol_pool().make("VecMap"))
             .unwrap();
-        let vec_map_instances =
-            if mono_info.is_used_datatype(env, targets, &vec_map_struct_env.get_qualified_id()) {
-                mono_info
-                    .structs
-                    .get(&vec_map_struct_env.get_qualified_id())
-                    .unwrap_or(&BTreeSet::new())
-                    .iter()
-                    .map(|tys| {
-                        (
-                            TypeInfo::new(env, options, &tys[0], false),
-                            TypeInfo::new(env, options, &tys[1], false),
-                        )
-                    })
-                    .collect_vec()
-            } else {
-                vec![]
-            };
+        let vec_map_instances = if mono_info.is_used_datatype(
+            env,
+            targets,
+            &vec_map_struct_env.get_qualified_id(),
+            &[],
+        ) {
+            mono_info
+                .structs
+                .get(&vec_map_struct_env.get_qualified_id())
+                .unwrap_or(&BTreeSet::new())
+                .iter()
+                .map(|tys| {
+                    (
+                        TypeInfo::new(env, options, &tys[0], false),
+                        TypeInfo::new(env, options, &tys[1], false),
+                    )
+                })
+                .collect_vec()
+        } else {
+            vec![]
+        };
         context.insert("vec_map_instances", &vec_map_instances);
     }
 
@@ -368,7 +378,7 @@ pub fn add_prelude(
             .find_struct(env.symbol_pool().make("TableVec"))
             .unwrap();
         let table_vec_instances =
-            if mono_info.is_used_datatype(env, targets, &table_vec_env.get_qualified_id()) {
+            if mono_info.is_used_datatype(env, targets, &table_vec_env.get_qualified_id(), &[]) {
                 mono_info
                     .structs
                     .get(&table_vec_env.get_qualified_id())