feat: dynamic field analysis on pures

crates/move-stackless-bytecode/src/dynamic_field_analysis.rs

@@ -601,15 +601,23 @@ impl FunctionTargetProcessor for DynamicFieldAnalysisProcessor {
 
     fn finalize(&self, env: &GlobalEnv, targets: &mut FunctionTargetsHolder) {
         // Collect and combine all functions' dynamic field info
-        let combined_info = DynamicFieldInfo::iter_union(targets.specs().filter_map(|fun_id| {
+        let combined_info = DynamicFieldInfo::iter_union(
             targets
-                .get_data(&fun_id, &FunctionVariant::Baseline)
-                .and_then(|data| {
-                    data.annotations
-                        .get::<DynamicFieldInfo>()
-                        .map(|info| info.clone())
-                })
-        }));
+                .specs()
+                .copied()
+                .chain(targets.get_funs().filter(|fun_id| {
+                    targets.is_pure_fun(fun_id) || targets.is_abort_check_fun(fun_id)
+                }))
+                .filter_map(|fun_id| {
+                    targets
+                        .get_data(&fun_id, &FunctionVariant::Baseline)
+                        .and_then(|data| {
+                            data.annotations
+                                .get::<DynamicFieldInfo>()
+                                .map(|info| info.clone())
+                        })
+                }),
+        );
 
         // Set the combined info in the environment
         env.set_extension(combined_info);

crates/sui-prover/tests/inputs/dynamic_field/pure_dynamic_field.ok.move

@@ -0,0 +1,25 @@
+module 0x42::foo;
+
+use prover::prover::{requires, ensures};
+
+use sui::dynamic_field;
+
+public struct Foo has key {
+    id: UID,
+}
+
+#[ext(pure)]
+fun has_field(x: &Foo): bool {
+    dynamic_field::exists_with_type<u64, u8>(&x.id, 10)
+}
+
+fun foo(x: &mut Foo) {
+    dynamic_field::add<u64, u8>(&mut x.id, 10, 42);
+}
+
+#[spec(prove)]
+fun foo_spec(x: &mut Foo) {
+    requires(!dynamic_field::exists_with_type<u64, u8>(&x.id, 10));
+    foo(x);
+    ensures(has_field(x));
+}

crates/sui-prover/tests/snapshots/dynamic_field/pure_dynamic_field.ok.move.snap

@@ -0,0 +1,5 @@
+---
+source: crates/sui-prover/tests/integration.rs
+expression: output
+---
+Verification successful