Support chained comparisons with evaluate-once semantics

[keyboardDrummer-bot]

PR requested and agreed on by @olivier-aws

Summary

Implements Option B from the design discussion in #892: desugar Python chained comparisons with temporary variables for intermediate operands to preserve evaluate-once semantics.

What changed

Strata/Languages/Python/PythonToLaurel.lean — Rewrote the Compare arm of translateExpr to handle chains of any length:

• Translates Compare(left, [op₁, ..., opₙ], [c₁, ..., cₙ]) into PAnd(left op₁ c₁, PAnd(c₁ op₂ c₂, ...)).
• For intermediate operands (all except the last comparator) that are not simple names or literals, introduces a LocalVariable temp binding so the operand is evaluated exactly once. For example, a < f() < b becomes:

  var cmp_tmp_<pos>_0 : Any := f();
  PAnd(PLt(a, cmp_tmp_<pos>_0), PLt(cmp_tmp_<pos>_0, b))
  

• Single comparisons (the common case) take the same code path with no temp variables and no Block wrapper, so there is no overhead for existing tests.

Test changes:

• Moved test_chained_compare.py from tests/pending/ to tests/ (now active).
• Added expected_laurel/test_chained_compare.expected with the verification output (all 5 checks pass).

Verification

• Full lake build succeeds.
• All 126 existing Python analysis tests pass (zero regressions).
• The new test_chained_compare test (assert 1 < x < 10) passes with all verification conditions satisfied.

Closes #892

[olivier-aws]

@keyboardDrummer-bot Try to get rid of the [i]! and change them to [i].

[keyboardDrummer-bot]

@olivier-aws Pushed a commit to remove all [i]! from the Compare translation section. Here's what changed:

• comparators.val[i]! → comparators.val[i] with a proven bound (have : i < comparators.val.size := by omega, using hComp and the loop membership proof).
• compExprs[i]!, operandRefs[i]!, pairs[i]! → .getD i hole where hole := mkStmtExprMd .Hole. These are mutable arrays built in for loops, so Lean can't track their sizes statically. getD returns a default instead of panicking — and the default is never actually reached since the sizes are correct by construction.
• Merged the if n > 1 then ... else ... branches into a single for h : i in [:n] loop, which simplifies the code and handles both cases uniformly.

lake build succeeds and all 155 Python analysis tests pass.

[tautschnig]

The test covers the basic 1 < x < 10 case (2-operator chain with simple operands). This exercises the PAnd chaining but not the temp variable path.

Consider adding tests for:

1. Side-effecting intermediate operand — e.g., a < f() < b to verify the temp variable is generated and the function is called once
2. Triple chain — e.g., 1 < x < y < 10 to verify longer chains work
3. Mixed operators — e.g., a <= b < c to verify different operators in the same chain

The first case is the most important since it's the core motivation for the evaluate-once semantics. Without it, the temp variable codepath is untested.

[keyboardDrummer-bot]

Added tests for cases 2 and 3:

• test_chained_compare_triple.py — 1 < x < y < 10 (3-operator chain, 7 VCs pass)
• test_chained_compare_mixed.py — a <= b < c (mixed operators, 5 VCs pass)

For case 1 (side-effecting intermediate operand): I tried a < f() < b and a < x + 0 < b, but both hit the downstream "local variables in functions are not YET supported" limitation in the Laurel-to-Core translator — the LocalVariable temp binding that the desugaring emits isn't supported there yet. So the temp variable codepath can't be end-to-end tested until that limitation is lifted. I think that's acceptable for now since the desugaring logic itself is straightforward, but happy to add a pending test for it if you'd prefer.

[keyboardDrummer-bot]

Addressed @tautschnig's review in 37e737c:

1. pairs.getD i hole → pairs[i]! — Switched to [i]! for consistency with the BoolOp fold. Removed the unused hole binding.

2. Added tests — test_chained_compare_triple (3-operator chain) and test_chained_compare_mixed (mixed <=/< operators). Both pass all VCs. The temp variable codepath (a < f() < b) can't be end-to-end tested yet due to a downstream "local variables in functions are not YET supported" limitation in the Laurel-to-Core translator.

3. isSimple conservatism — Left as-is. The extra temp variable for .Attribute nodes is harmless for correctness and avoids potential unsoundness from __getattr__ overrides.

Build passes, all 157 tests green (including the 2 new ones).

[keyboardDrummer-bot]

Thanks for the review and approval @tautschnig! All feedback has been addressed. Ready to merge whenever @olivier-aws is happy with it.

[robin-aws]

A few thoughts for later (especially since this is my first Strata review) but I'm just fine with this being merged as is.

[robin-aws]

(Non blocking) This seems generically useful enough to move to Util.lean later instead

[robin-aws]

For later, it would be incredibly valuable to actually prove that this pattern of fresh variable creation is actually sound and can't conflict with existing variables (shadowing may be fine)

[robin-aws]

Two points where I think we can easily improve the testing coverage here. Not blocking but following up afterwards (and improving this more broadly) would be great.

1. There's no actual test of the critical point of evaluating each operand only once. That wouldn't be complicated to do at the Python level by including x < f() < y and defining f() to return different values if invoked multiple times. If that turns out to be impossible because the operands HAVE to be pure, then we should find another way to assert f is only evaluated once. Even if we only want to evaluating operands only once for performance reasons, we still have to test for that somehow.
2. In general, it looks like all of our test cases are only including assert statements that are expected to pass. IME this doesn't guard against several ways to accidentally break analysis such that it always succeeds. I would argue every test case should have at least one assert expected to fail as well, or else we have a pretty big blind spot in testing. (This is especially on my mind because with the test cases we have so far, I believe I could write a core interpreter that pass all of them by doing absolutely no actual execution :)