Dynamic field UID Fix by andrii-a8c · Pull Request #534 · asymptotic-code/sui-prover

andrii-a8c · 2026-02-24T15:13:20Z

Initial commit made by cursor

Resolves: #535
Resolves: #536

cursor · 2026-02-24T15:13:24Z

You have run out of free Bugbot PR reviews for this billing cycle. This will reset on March 1.

To receive reviews on all of your PRs, visit the Cursor dashboard to activate Pro and start your 14-day free trial.

Copilot

Pull request overview

This PR updates the Move Prover’s dynamic-field pipeline to better handle cases where UID is passed directly as a function parameter, and extends the Boogie prelude/backend to cover additional dynamic-field operations.

Changes:

Extend DynamicFieldAnalysis with inter-procedural handling of UID parameters and call-site type substitution.
Add Boogie prelude/backend support for dynamic_field::remove_if_exists and ensure dynamic-field-related types aren’t translated as opaque.
Add new sui-prover integration test inputs and snapshots covering UID-parameter scenarios.

Reviewed changes

Copilot reviewed 12 out of 13 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
crates/move-stackless-bytecode/src/dynamic_field_analysis.rs	Adds UID-parameter tracking and call-site-based type resolution/substitution during dynamic field analysis.
crates/move-prover-boogie-backend/src/boogie_backend/prelude/native.bpl	Introduces a Boogie procedure template for `remove_if_exists`.
crates/move-prover-boogie-backend/src/boogie_backend/lib.rs	Threads `remove_if_exists` into dynamic-field instance generation; adjusts instance inclusion logic (incl. UID).
crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs	Changes opaque-type decision to keep dynamic-field-bearing structs non-opaque.
crates/sui-prover/tests/inputs/dynamic_field/*.move	Adds new Move inputs to exercise UID parameter behavior and remove/exists variants.
crates/sui-prover/tests/snapshots/dynamic_field/*.snap	Adds snapshots asserting successful verification for the new inputs.
Cargo.lock	Updates dependency lockfile due to upstream/version changes.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

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

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

andreistefanescu

let's split the changes from dynamic_field_analysis from the rest

crates/move-prover-boogie-backend/src/boogie_backend/prelude/native.bpl

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

…c field analysis When a function takes &UID directly (rather than extracting from an object), the analysis can't determine the parent object type. Instead of emitting an error (E0022), fall back to placing dynamic fields under UID itself with a warning. If any dynamic field for a UID needs fallback, all fields for that UID use UID type for consistency. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

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

When a function mixes direct UID usage (from inlined callees taking &UID) with obj.id access, consolidate all dynamic field entries under UID type to ensure consistent Boogie slots. Simplifies compute_uid_info by removing UID parameter tracking and FreezeRef/ReadRef/Assign propagation. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…ngs emitted When any function uses the UID fallback (warning emitted), finalize now consolidates all dynamic field entries under UID type — both the global combined_info and each function's per-function annotation. This ensures consistent Boogie slots across the entire program. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…ard in process The annotation consolidation (merging all df entries under UID type) is handled entirely by finalize. Process only keeps the bytecode rewriting guard (use_uid_type) since type_inst must match the consolidated annotations and bytecodes can't be rewritten after emission. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

The uid_fallback closure in info collection already handles the case where parent is unknown, and the use_uid_type guard ensures bytecode consistency. The extra else-if branch was redundant. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Move UID detection to initialize (runs before process). When any accessible function takes &UID and makes df calls, set a global flag. Process then routes all df operations through UID type directly. Finalize no longer needs to consolidate annotations or bytecodes. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…pen-type filter Finalize now collects from all functions (like main) instead of just specs/pure/abort-check. Removed the per-function and global annotation consolidation (handled by initialize + process). Kept the fixpoint loop for UID entry propagation (needed when reachable functions skip callee propagation) and open-type filtering (prevents ill-founded Boogie types). Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

…alysis Allow callee info propagation for reachable functions so generic instantiation flows naturally through call chains. This eliminates the need for the fixpoint loop in finalize. Gracefully skip callees that were filtered out (spec functions) instead of panicking. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

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

Instead of checking if a function has a UID parameter, actually try resolving each df call's parent object type using the same logic as compute_uid_info (BorrowField/GetField + callee propagation). Only flag as unresolvable when resolution genuinely fails. Callee uid_info is computed recursively on-the-fly since annotations don't exist yet in initialize. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

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

…or type params used in UID dynamic fields Instead of filtering open-typed UID entries in dynamic field analysis finalize, prevent the circularity at the source: don't generate UID-wrapping datatype declarations for type parameters that appear in UID's dynamic field entries. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

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

…ations When a dynamic field value type is a compound type like Vec(T), it must be parenthesized inside Table declarations to avoid Boogie parsing it as extra type arguments. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

… 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>

Structs with dynamic fields must not be opaque. Move this check from the struct translation loop into MonoInfo::is_used_datatype so the logic is centralized. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Dynamic field UID fix

80946f3

andrii-a8c requested a review from andreistefanescu February 24, 2026 15:13

andrii-a8c self-assigned this Feb 24, 2026

Copilot AI review requested due to automatic review settings February 24, 2026 15:13

Copilot started reviewing on behalf of andrii-a8c February 24, 2026 15:13 View session

Copilot AI reviewed Feb 24, 2026

View reviewed changes

feat: cleanup

58462ac

andreistefanescu requested changes Feb 24, 2026

View reviewed changes

crates/move-prover-boogie-backend/src/boogie_backend/prelude/native.bpl Outdated Show resolved Hide resolved

crates/move-prover-boogie-backend/src/boogie_backend/lib.rs Outdated Show resolved Hide resolved

andrii-a8c added 5 commits February 26, 2026 01:04

Merge branch 'main' into dynamic-field-uid-fix

b07fb89

feat: refractor + bpl fix

f505364

Merge branch 'main' into dynamic-field-uid-fix

0bd8938

Merge branch 'main' into dynamic-field-uid-fix

daf7d57

removed unrelated

d0679d3

andrii-a8c requested a review from andreistefanescu February 26, 2026 10:13

andrii-a8c changed the title ~~Dynamic field UID fix~~ Dynamic field UID Fix Feb 26, 2026

andrii-a8c and others added 14 commits February 26, 2026 20:27

Merge branch 'main' into dynamic-field-uid-fix

482415e

restore comments removed in earlier commits

a47c962

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

refactor: use Cell<bool> field instead of env extension for use_uid flag

b95eec7

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

refactor: clarify finalize open-type filter comment

662444c

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

Merge origin/main into dynamic-field-uid-fix

fa418b8

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

andreistefanescu and others added 5 commits March 13, 2026 19:09

remove unused is_open method from NameValueInfo

b167539

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

refactor: move dynamic field opaqueness check into is_used_datatype

54d4938

Structs with dynamic fields must not be opaque. Move this check from the struct translation loop into MonoInfo::is_used_datatype so the logic is centralized. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

andreistefanescu approved these changes Mar 16, 2026

View reviewed changes

andreistefanescu merged commit 1e66596 into main Mar 16, 2026
13 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Dynamic field UID Fix#534

Dynamic field UID Fix#534
andreistefanescu merged 26 commits intomainfrom
dynamic-field-uid-fix

andrii-a8c commented Feb 24, 2026 •

edited

Loading

Uh oh!

cursor bot commented Feb 24, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

andreistefanescu left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

andrii-a8c commented Feb 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

cursor bot commented Feb 24, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

andreistefanescu left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

andrii-a8c commented Feb 24, 2026 •

edited

Loading