[prover] Fix signed integer division semantics in Move Prover#18580
Draft
[prover] Fix signed integer division semantics in Move Prover#18580
Conversation
GotenJBZ
changed the title
Contributor
There was a problem hiding this comment.
Pull request overview
This PR fixes incorrect verification behavior in the Move Prover for signed integer division and modulo operations. Boogie's built-in div/mod operators use floor division semantics, while Move/Rust use truncation division, causing verification failures when negative operands are involved.
Changes:
- Added
$truncDivand$truncModhelper functions implementing truncation semantics - Updated
$Divand$Modprocedures to use truncation logic - Modified spec_translator to call truncation helpers for non-bitvector division/modulo operations
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
| third_party/move/move-prover/boogie-backend/src/prelude/prelude.bpl | Implements truncation division/modulo functions and updates $Div/$Mod procedures |
| third_party/move/move-prover/boogie-backend/src/spec_translator.rs | Routes Div/Mod operations through new truncation helpers |
| third_party/move/move-prover/tests/sources/functional/signed_int/signed_div_cast.move | Adds functional test for signed division with casts |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
third_party/move/move-prover/boogie-backend/src/prelude/prelude.bpl
Outdated
Show resolved
Hide resolved
third_party/move/move-prover/tests/sources/functional/signed_int/signed_div_cast.move
Show resolved
Hide resolved
rahxephon89
reviewed
Feb 3, 2026
third_party/move/move-prover/boogie-backend/src/prelude/prelude.bpl
Outdated
Show resolved
Hide resolved
GotenJBZ
force-pushed
the
fix-signed-div-mod-semantics
branch
from
ac9a143 to
fe474df
Compare
rahxephon89
approved these changes
Feb 3, 2026
junxzm1990
reviewed
Feb 3, 2026
junxzm1990
approved these changes
Feb 4, 2026
GotenJBZ
force-pushed
the
fix-signed-div-mod-semantics
branch
from
f5721d1 to
78fecc4
Compare
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
This comment has been minimized.
Contributor
✅ Forge suite
|
Contributor
✅ Forge suite
|
Contributor
✅ Forge suite
|
Boogie's built-in div/mod operators use floor division, while Move/Rust use truncation division. This causes incorrect verification for signed integers with negative operands. Add $truncDiv and $truncMod functions to implement truncation semantics and update spec_translator to use them for div/mod operations.
GotenJBZ
force-pushed
the
fix-signed-div-mod-semantics
branch
from
78fecc4 to
64df3f6
Compare
junxzm1990
reviewed
Feb 5, 2026
third_party/move/move-prover/boogie-backend/src/prelude/prelude.bpl
Outdated
Show resolved
Hide resolved
GotenJBZ
force-pushed
the
fix-signed-div-mod-semantics
branch
from
0afd265 to
10340ce
Compare
wrwg
requested changes
Feb 6, 2026
| // When src1 < 0 and src2 < 0 and not exact: trunc = euc - 1 | ||
| if ( src1 >= 0 ) then | ||
| src1 div src2 | ||
| else if (src1 mod src2 == 0) then |
Contributor
There was a problem hiding this comment.
This has two division ops (mod and div) in strict execution path which is very expensive for SMT solving.
Why don't we do
if (src1 >= 0 && src2 >= 0) { <<old code>> } else { <<new code>> }
... as I suggested? Then all existing verification or uNN do the same as before (just a little comparison tests). Signed ints are very new and we hit the more expensive case only then.
Again: it is super important to minimize the number of division/mod/mul ops for SMT preformance.
Correct $truncDiv and $truncMod in the Boogie prelude to properly handle cases where src2 < 0 or src1 >= 0 with negative src2. The previous implementation only checked src1 >= 0 in the fast path, which was incorrect when src2 < 0. Update baseline expectation for loops_with_memory_ops accordingly. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
Bugbot Autofix is OFF. To automatically fix reported issues with Cloud Agents, enable Autofix in the Cursor dashboard.
| self.translate_exp(&args[1]); | ||
| emit!(self.writer, ")"); | ||
| } | ||
| } |
There was a problem hiding this comment.
Bitwise branch duplicated between translate_op and translate_trunc_div_mod_op
Low Severity
The Bitwise branch in translate_trunc_div_mod_op (lines 2097–2105) is an exact copy of the Bitwise branch in translate_op (lines 2073–2081). Only the else branches differ between the two methods. This duplication risks the two methods diverging if the bitvector emission logic is updated in one but not the other. The shared Bitwise handling could be extracted into a helper, with each method only providing its own non-Bitwise logic.
Additional Locations (1)
GotenJBZ
requested review from
a team,
JoshLind,
alinush,
grao1991,
gregnazario,
lightmark,
rex1fernando and
waamm
as code owners
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Boogie's built-in div/mod operators use floor division, while Move/Rust use truncation division. This causes incorrect verification for signed integers with negative operands.
Add $truncDiv and $truncMod functions to implement truncation semantics and update spec_translator to use them for div/mod operations.
Description
How Has This Been Tested?
Key Areas to Review
Type of Change
Which Components or Systems Does This Change Impact?
Checklist
Note
High Risk
High risk because it introduces automated deletion of state Merkle stale nodes via a new background cleaner and adds new allocator configuration paths (jemalloc), both of which can impact node stability and data integrity if misconfigured.
Overview
Adds a new state tree debugging command (
check_stale_nodes) plus a background leaked stale node cleanup worker (leaked_stale_node_cleaner) that snapshots pruner progress, iterates shard/metadata DBs, and batch-deletesJellyfishMerkleNode+ stale-index entries up to persisted target versions.Introduces a new
aptos-jemalloccrate with asetup_jemalloc!macro (global allocator +malloc_conf) and an optional metrics collection thread exportingaptos_jemalloc_bytes; also addsTelemetryServiceConfigwith a configurable/default thread count.Expands Move and crypto test coverage: new e2e tests for
crypto_algebratype-tag budget handling and gas-profiler HTML report generation, new randomness smoke tests (fast-path on/off + optimistic verification scenarios), neworder_id_generationframework module (bit-reversed monotonic order IDs) with tests, additional trading bulk order validation tests, and a large set of new Move bytecode verifier transactional tests. Also adds DKG crypto types/serialization utilities (Subtranscriptaggregation + sigmaProofenum serialization) and new docker builder scripts for CLI/perf profiles.Written by Cursor Bugbot for commit 726fac2. This will update automatically on new commits. Configure here.