Support bitwise ~, <<, >> operators in Python frontend

[keyboardDrummer-bot]

PR asked and pushed by @olivier-aws

Summary

Implements Option B from the design discussion in #893: inline arithmetic identities in the Python Laurel runtime functions to support bitwise ~, <<, and >> operators.

Approach

The three operators are modeled using exact arithmetic identities for Python's arbitrary-precision integers:

• ~x → -(x + 1) (exact for arbitrary-precision integers)
• x << n → x * int_pow(2, n) (for n ≥ 0)
• x >> n → x / int_pow(2, n) (for n ≥ 0, using integer division)

Negative shift detection

Per @olivier-aws's request, PLShift and PRShift include requires clauses that enforce n >= 0. When the verifier cannot prove the shift amount is non-negative, it flags this as a potential issue — matching Python's runtime behavior of raising ValueError for negative shift counts.

Changes

File	Change
PythonToLaurel.lean	Map Invert → PBitNot, LShift → PLShift, RShift → PRShift
PythonRuntimeLaurelPart.lean	Add PBitNot, PLShift, PRShift runtime functions
PythonRuntimeLaurelPart.lean	Add new functions to AnyMaybeExceptionList
tests/pending/ → tests/	Move test_bitnot.py, test_lshift.py, test_rshift.py
expected_laurel/	Add .expected files for the three tests

Verification

• All 3 new tests pass ✅
• Full test suite (157 tests) passes with no regressions ✅
• --check-pending confirms 0 pending tests accidentally promoted ✅
• Negative shift amounts are correctly flagged as inconclusive when the verifier can't prove n >= 0 ✅

Closes #893

[olivier-aws]

@keyboardDrummer-bot Add tests for the negative shift case. These tests should catch an error when the right operand is negative.

[keyboardDrummer-bot]

@olivier-aws Added two tests for negative shift amounts in dbc60bf:

• test_lshift_negative.py — x << -1 → flagged as inconclusive (3 inconclusive checks)
• test_rshift_negative.py — x >> -1 → flagged as inconclusive (3 inconclusive checks)

Both tests confirm that the requires clauses on PLShift/PRShift correctly catch negative shift operands. The verifier cannot prove n >= 0 when the shift amount is -1, so the checks are reported as inconclusive — matching the expected behavior (Python raises ValueError for negative shifts at runtime).

Verified locally:

• All 4 shift tests pass (positive + negative for both << and >>) ✅
• Full test suite: 159 tests pass, 0 failures ✅
• --check-pending: 0 pending tests accidentally promoted ✅

[keyboardDrummer-bot]

CI fix pushed

The "Build and test Lean (stable)" check was failing because PreludeVerifyTest couldn't verify the prelude after adding PLShift/PRShift. Root cause was two issues:

1. requires clauses blocked AnyMaybeExcept proof. The requires clauses on PLShift/PRShift prevented the verifier from proving that these functions propagate exceptions from their arguments (the AnyMaybeExcept property). The verifier generates WF-checking procedures that call the function with exception arguments, but the requires clause can't be satisfied in that context.

2. PRShift used / which becomes Int.SafeDiv. The Laurel / operator translates to Int.SafeDiv in Core, which has a precondition that the divisor is non-zero. The verifier couldn't prove int_pow(2, n) != 0 because int_pow is an uninterpreted external function.

Fix

• Removed requires clauses from PLShift and PRShift. Negative shift amounts are now guarded with inline && Any..as_int!(v2) >= 0 conditions (matching the PPow pattern). When the shift amount is negative, the function falls through to the UndefinedError exception branch, which still causes the verifier to flag the issue as inconclusive.

• Introduced int_rshift external function for PRShift to avoid Int.SafeDiv entirely. Added intRshiftFunc to PyFactory with concreteEval for constant folding (computes floor(x / 2^n) for concrete values).

• Updated expected test outputs for test_lshift, test_rshift, test_lshift_negative, and test_rshift_negative to reflect the removal of requires-based WF checks.

Verification

• PreludeVerifyTest ✅ passes
• All 159 Python analyze tests pass (including the 5 new bitwise operator tests)
• Full lake test has only 2 pre-existing failures unrelated to this PR (Java.TestGen missing jar, AnalyzeLaurelTest regex/bucket tests that also fail on the parent commit)

[keyboardDrummer-bot]

Thanks for the review @MikaelMayer! Here's a summary of how I addressed each comment:

Nits (fixed in 22924d7):

• ✅ Updated section header from "Modelling of other Python operations, currrently unsupported" → "Modelling of Python arithmetic and bitwise operations"
• ✅ Updated the external function comment to mention int_rshift alongside int_pow and float_pow, and updated the reference to say PPow/PRShift

Soundness questions (answered inline):

• PBitNot (line 620): exception is correct — Python's ~ only works on int/bool, all other built-in types raise TypeError
• PLShift/PRShift (line 984): exception is correct — Python's <</>> only work on int/bool, no implicit conversions exist for other built-in types

I noted in the inline replies that if we want to be conservative about user-defined classes with custom __invert__/__lshift__/__rshift__, we could use hole instead, but that would be a broader policy change affecting existing functions like PNot too. Happy to discuss if you'd like to go that route.

[joehendrix]

I added one clarifying question, but it's more about the expected_laurel directory and how to know when the expected output is correct.