fix: cross module assert

[d3mage]

Fixes #147

---

Note

Adds tests verifying cross-module asserts succeed in targeted specs and that asserts in scenario specs produce the expected error.

• Tests:
  • Cross-module assert (success): Add tests/inputs/assert.ok.move targeting 0x42::foo::foo from 0x43::bar::foo_spec; snapshot snapshots/assert.ok.move.snap expects "Verification successful".
  • Scenario spec (failure): Add tests/inputs/assert.scenario.fail.move with scenario_spec using asserts; snapshot snapshots/assert.scenario.fail.move.snap expects bytecode transformation error about scenario specs and asserts.

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

[Copilot]

Pull Request Overview

This PR fixes an issue with cross-module assert handling in the Move prover by ensuring assert functions are properly processed when called from different modules.

• Adds a new condition to handle asserts calls in Default translation style
• Updates test case to verify cross-module assert functionality works correctly
• Includes a minor formatting adjustment to improve code readability

Reviewed Changes

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

File	Description
crates/sui-prover/tests/inputs/assert.ok.move	Adds test case demonstrating cross-module assert usage with prover spec
crates/sui-prover/tests/snapshots/assert.ok.move.snap	Expected test output snapshot showing successful verification
crates/move-prover-boogie-backend/src/boogie_backend/bytecode_translator.rs	Fixes assert processing logic and minor formatting cleanup

---

_{Tip: Customize your code reviews with copilot-instructions.md. Create the file or learn how to get started.}

[andreistefanescu]

@d3mage let's update this to include #351, which throws an error is there are asserts in a scenario spec

[cursor]

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.

[andreistefanescu]

@andrii-a8c I think we can revert the code change, just keep the tests

[andreistefanescu]

👍