test: add tests for UID fallback, circular datatype fix, and compound type parenthesization

- uid_param_vec_value: UID fallback + vector value type (parenthesization)
- uid_param_multi_type_params: multiple type params on &UID (circular fix)
- uid_param_multi_ops: multiple df operations with different types on same &UID
- uid_param_nested_generic: generic calling generic on &UID (transitive fallback)
- vec_value_concrete: vector value type on normal object (parenthesization)

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: andreistefanescu

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

@@ -0,0 +1,26 @@
+module 0x42::foo;
+
+use prover::prover::{requires, ensures};
+use sui::dynamic_field as df;
+
+public struct NameKey has copy, store, drop {}
+public struct CountKey has copy, store, drop {}
+
+public struct MyObject has key {
+    id: UID,
+}
+
+public fun initialize(uid: &mut UID, count: u64) {
+    df::add<NameKey, bool>(uid, NameKey {}, true);
+    df::add<CountKey, u64>(uid, CountKey {}, count);
+}
+
+#[spec(prove)]
+fun verify_initialize(obj: &mut MyObject, count: u64) {
+    requires(!df::exists_with_type<NameKey, bool>(&obj.id, NameKey {}));
+    requires(!df::exists_with_type<CountKey, u64>(&obj.id, CountKey {}));
+    initialize(&mut obj.id, count);
+    ensures(df::exists_with_type<NameKey, bool>(&obj.id, NameKey {}));
+    ensures(df::exists_with_type<CountKey, u64>(&obj.id, CountKey {}));
+    ensures(*df::borrow<CountKey, u64>(&obj.id, CountKey {}) == count);
+}

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

@@ -0,0 +1,24 @@
+module 0x42::foo;
+
+use prover::prover::{requires, ensures};
+use sui::dynamic_field as df;
+
+public struct MyObject has key {
+    id: UID,
+}
+
+public fun generic_add<K: copy + store + drop, V: store>(uid: &mut UID, key: K, val: V) {
+    df::add<K, V>(uid, key, val);
+}
+
+public fun generic_exists<K: copy + store + drop, V: store>(uid: &UID, key: K): bool {
+    df::exists_with_type<K, V>(uid, key)
+}
+
+#[spec(prove)]
+fun generic_add_u64_bool_spec(obj: &mut MyObject, key: u64, val: bool) {
+    requires(!df::exists_with_type<u64, bool>(&obj.id, key));
+    generic_add<u64, bool>(&mut obj.id, key, val);
+    ensures(df::exists_with_type<u64, bool>(&obj.id, key));
+    ensures(*df::borrow<u64, bool>(&obj.id, key) == val);
+}

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

@@ -0,0 +1,29 @@
+module 0x42::foo;
+
+use prover::prover::{requires, ensures};
+use sui::dynamic_field as df;
+
+public struct MyObject has key {
+    id: UID,
+}
+
+public fun has_field<K: copy + store + drop, V: store>(uid: &UID, key: K): bool {
+    df::exists_with_type<K, V>(uid, key)
+}
+
+public fun get_field<K: copy + store + drop, V: store + copy + drop>(uid: &UID, key: K, default: V): V {
+    if (has_field<K, V>(uid, key)) {
+        *df::borrow<K, V>(uid, key)
+    } else {
+        default
+    }
+}
+
+#[spec(prove)]
+fun verify_get_field(obj: &MyObject, key: u64): u64 {
+    requires(df::exists_with_type<u64, u64>(&obj.id, key));
+    requires(*df::borrow<u64, u64>(&obj.id, key) == 42);
+    let result = get_field<u64, u64>(&obj.id, key, 0);
+    ensures(result == 42);
+    result
+}

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

@@ -0,0 +1,20 @@
+module 0x42::foo;
+
+use prover::prover::{requires, ensures};
+use sui::dynamic_field as df;
+
+public struct MyObject has key {
+    id: UID,
+}
+
+public fun set_scores(uid: &mut UID, key: u64, scores: vector<u64>) {
+    df::add(uid, key, scores);
+}
+
+#[spec(prove)]
+fun verify_set_scores(obj: &mut MyObject, key: u64, scores: vector<u64>) {
+    requires(!df::exists_with_type<u64, vector<u64>>(&obj.id, key));
+    set_scores(&mut obj.id, key, scores);
+    ensures(df::exists_with_type<u64, vector<u64>>(&obj.id, key));
+    ensures(*df::borrow<u64, vector<u64>>(&obj.id, key) == scores);
+}

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

@@ -0,0 +1,20 @@
+module 0x42::foo;
+
+use prover::prover::{requires, ensures};
+use sui::dynamic_field as df;
+
+public struct Foo has key {
+    id: UID,
+}
+
+fun store_list(x: &mut Foo, key: u64, items: vector<u64>) {
+    df::add<u64, vector<u64>>(&mut x.id, key, items);
+}
+
+#[spec(prove)]
+fun store_list_spec(x: &mut Foo, key: u64, items: vector<u64>) {
+    requires(!df::exists_with_type<u64, vector<u64>>(&x.id, key));
+    store_list(x, key, items);
+    ensures(df::exists_with_type<u64, vector<u64>>(&x.id, key));
+    ensures(*df::borrow<u64, vector<u64>>(&x.id, key) == items);
+}

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

@@ -0,0 +1,16 @@
+---
+source: crates/sui-prover/tests/integration.rs
+expression: output
+---
+Verification successful
+warning: UID object type not found, dynamic fields will be placed under UID
+   ┌─ tests/inputs/dynamic_field/uid_param_multi_ops.ok.move:14:5
+   │
+14 │     df::add<NameKey, bool>(uid, NameKey {}, true);
+   │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+warning: UID object type not found, dynamic fields will be placed under UID
+   ┌─ tests/inputs/dynamic_field/uid_param_multi_ops.ok.move:15:5
+   │
+15 │     df::add<CountKey, u64>(uid, CountKey {}, count);
+   │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

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

@@ -0,0 +1,10 @@
+---
+source: crates/sui-prover/tests/integration.rs
+expression: output
+---
+Verification successful
+warning: UID object type not found, dynamic fields will be placed under UID
+   ┌─ tests/inputs/dynamic_field/uid_param_multi_type_params.ok.move:11:5
+   │
+11 │     df::add<K, V>(uid, key, val);
+   │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^

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

@@ -0,0 +1,16 @@
+---
+source: crates/sui-prover/tests/integration.rs
+expression: output
+---
+Verification successful
+warning: UID object type not found, dynamic fields will be placed under UID
+   ┌─ tests/inputs/dynamic_field/uid_param_nested_generic.ok.move:16:10
+   │
+16 │         *df::borrow<K, V>(uid, key)
+   │          ^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+warning: UID object type not found, dynamic fields will be placed under UID
+   ┌─ tests/inputs/dynamic_field/uid_param_nested_generic.ok.move:11:5
+   │
+11 │     df::exists_with_type<K, V>(uid, key)
+   │     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

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

@@ -0,0 +1,10 @@
+---
+source: crates/sui-prover/tests/integration.rs
+expression: output
+---
+Verification successful
+warning: UID object type not found, dynamic fields will be placed under UID
+   ┌─ tests/inputs/dynamic_field/uid_param_vec_value.ok.move:11:5
+   │
+11 │     df::add(uid, key, scores);
+   │     ^^^^^^^^^^^^^^^^^^^^^^^^^

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

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