Always use Boogie function form for pure callees

[andreistefanescu]

• Simplify condition to always use use_func = true when callee is pure
• Add SMT-level tests for pure functions with conditionals

---

Note

Medium Risk
Changes how pure Move calls are lowered to Boogie (function vs procedure) and which $pure/$impl/$opaque variant gets invoked, which can affect verification behavior and existing proofs. Added tests reduce regression risk but translation changes may surface new prover differences.

Overview
Pure callees are now always emitted using Boogie function form, simplifying the previous style-dependent gating and making pure-call lowering more consistent.

Spec-call name resolution is adjusted to prefer the $pure variant whenever available (including when using Opaque translation with use_impl), falling back to $impl/$opaque only when needed.

Adds new sui-prover SMT-level tests (and snapshots) covering pure functions with conditionals and a case where a valid pure function fails only at SMT due to an intentionally false ensures.

^{Written by Cursor Bugbot for commit b4f81b7. This will update automatically on new commits. Configure here.}

[Copilot]

Pull request overview

This PR simplifies the logic for translating pure function calls to Boogie by ensuring pure callees always use the Boogie function form, removing unnecessary conditional checks.

Changes:

• Simplified the condition for setting use_func = true when a callee is pure, removing redundant style checks
• Added SMT-level test cases for pure functions with conditionals to verify correct behavior

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs	Simplified condition to always use function form for pure callees
crates/sui-prover/tests/inputs/pure_functions/pure_smt_verification.fail.move	Added test case with false logical claim in spec for pure function
crates/sui-prover/tests/inputs/pure_functions/pure_conditional_smt.ok.move	Added test case with valid pure function containing conditionals
crates/sui-prover/tests/inputs/pure_functions/pure_conditional_smt.fail.move	Added test case with buggy pure function implementation
crates/sui-prover/tests/snapshots/pure_functions/pure_smt_verification.fail.move.snap	Snapshot for expected verification error output
crates/sui-prover/tests/snapshots/pure_functions/pure_conditional_smt.ok.move.snap	Snapshot for expected successful verification output
crates/sui-prover/tests/snapshots/pure_functions/pure_conditional_smt.fail.move.snap	Snapshot for expected verification error with buggy implementation

---

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

[cursor]

Cursor Bugbot has reviewed your changes and found 2 potential issues.

^{Bugbot Autofix is OFF. To automatically fix reported issues with Cloud Agents, enable Autofix in the Cursor dashboard.}

This PR is being reviewed by Cursor Bugbot

Details

Your team is on the Bugbot Free tier. On this plan, Bugbot will review limited PRs each billing cycle for each member of your team.

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

[cursor]

Missing suffix for pure callees in some translation styles

Medium Severity

The condition for setting use_func = true was simplified to apply to all translation styles when callee_is_pure is true. However, the suffix logic for spec calls only handles Default+Verification, SpecNoAbortCheck, and Opaque styles. For spec calls in Asserts or Aborts styles (newly affected by this change), use_func becomes true but no $pure suffix is appended to fun_name, potentially calling the wrong Boogie function variant.

Additional Locations (1)

• crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs#L3894-L3928

 

[cursor]

Redundant is_pure_fun checks duplicate existing variable

Medium Severity

The is_pure_fun check at lines 3903-3906 and 3916-3919 duplicates the already-computed callee_is_pure variable (line 3759). The method can_callee_be_function(mid, fid) used to compute callee_is_pure is defined as self.parent.targets.is_pure_fun(&mid.qualified(*fid)), which is semantically identical. Replace self.parent.targets.is_pure_fun(&QualifiedId { module_id: *mid, id: *fid }) with callee_is_pure.