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.