Enhance div_xy_y to support signed and unsigned division simplification

[sidarth16]

Summary

This PR updates the div_xy_y helper to handle simplifications for both unsigned (DIV) and signed (SDIV) EVM operations. It allows expressions like (x * y) / x or (x * y) / y to be simplified automatically, improving symbolic reasoning and reducing complexity in arithmetic analysis.

Changes

• Added signed: bool parameter to div_xy_y.
• Implemented simplification logic for SDIV (signed division).
• Preserved unsigned simplification logic with overflow checks.
• Updated arith to call div_xy_y for both DIV and SDIV before falling back to generic operations.

Notes

• This is an internal optimization; outputs remain identical to previous behavior.
• Existing unit tests cover correctness; no new tests are added in this PR.

[0xkarmacoma]

thanks @sidarth16, note that it would cool to add a couple unit tests to verify the functionality

deferring to @daejunpark for the actual div_xy_y logic safety.

[Copilot]

Pull Request Overview

This PR enhances the div_xy_y helper function to handle simplifications for both unsigned (DIV) and signed (SDIV) EVM operations. The enhancement allows expressions like (x * y) / x or (x * y) / y to be simplified automatically, improving symbolic reasoning performance in arithmetic analysis.

Key changes:

• Extended div_xy_y to support signed division with a new signed parameter
• Updated the arithmetic operation handler to use div_xy_y for both DIV and SDIV operations
• Removed TODO comments indicating this functionality was planned

Reviewed Changes

Copilot reviewed 2 out of 4 changed files in this pull request and generated 6 comments.

File	Description
src/halmos/sevm.py	Enhanced div_xy_y with signed division support and integrated it into DIV/SDIV operations
src/halmos/bitvec.py	Removed TODO comments for division simplification functionality