Add signed add overflow elimination coverage

[augmentcode]

Problem

• Signed safeadd had no overflow-elimination coverage, so we weren't exercising the VRA-proven-safe path or the sign-boundary guard.

Solution

• Teach OverflowEliminationPass to recognize the signed eq(slt(y, 0), slt(add(x, y), x)) check and add unit coverage for both elimination and non-elimination.

Misc

• Manual session fallback: github-api was unavailable, so this PR was opened via github-app-api.

---

Pull Request opened by Augment Code | View session

[augmentcode]

^{PR Author Agent⚡}

👋 I've got this PR.

I'll handle review feedback, CI failures, and merge conflicts, and ping you the moment it's ready for review. Drop a comment anytime.

Marking it ready and picking reviewers are your call — I'll leave both alone.

[augmentcode]

^{Deep Code Review Agent🐛}

Review completed with 1 suggestions.

[augmentcode]

The test name test_no_eliminate_signed_add_overflow_crossing_sign_boundary suggests testing addition across positive/negative boundaries, but mod produces only non-negative values [0, 2^254], so both x and y are non-negative and slt %y, 0 is always false; the test actually validates that the pass correctly rejects elimination when max(x) + max(y) > SIGNED_MAX (2^255 > 2^255-1), not sign-boundary crossing.

Severity: low

---

_{🤖 Was this useful? React with 👍 or 👎}

[augmentcode]

^{PR Author Agent⚡}

Good catch — I renamed the test to test_no_eliminate_signed_add_overflow_exceeding_signed_max and updated the docstring to match what the setup is actually proving in a2bdf9a.

[augmentcode]

^{PR Author Agent⚡}

This PR appears to be inactive. The agent will stop monitoring until a new comment is posted.