fix: preserve mutation path in opaque spec calls (#545)

[andreistefanescu]

Fixes #545

When calling an opaque spec function with &mut parameters, the mutation's path must be preserved. Three cases fixed:

1. Function-style deterministic opaque: wrap with $UpdateMutation
2. Datatypes multiple returns: wrap &mut extractions with $UpdateMutation
3. Procedure-style non-deterministic: save &mut refs before call, restore paths after

No seen set needed since all mutable sources are distinct due to Rust borrow rules.

Generated with Claude Code) • [claude/issue-545-20260306-2352](https://github.com/asymptotic-code/sui-prover/tree/claude/issue-545-20260306-2352

[cursor]

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

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

[andreistefanescu]

@claude fix the test

[claude]

Claude finished @andreistefanescu's task in 5m 46s —— View job

---

Fixed the test

• Read the new test file to understand the expected behavior
• Run the test to see the failure
• Fix the test (create missing snapshot)
• Commit and push

The test move_test__opaque_framing_ok was failing because the snapshot file was missing. I checked the CI logs which confirmed the test verifies successfully (all checks pass: SpecNoAbortCheck, frame_Check, frame_Assume, frame_SpecNoAbortCheck) but there was no .snap file to compare against.

Created crates/sui-prover/tests/snapshots/opaque/framing.ok.move.snap with the expected output Verification successful, matching the format of other opaque test snapshots.
• Branch