Support multiple assignment targets in Python frontend

[keyboardDrummer-bot]

PR requested and agreed on by @olivier-aws

Desugar a = b = 5 (and a = b = c = 1, etc.) into individual assignments for each target, all sharing the same RHS expression. This removes the "Multiple assignment targets not yet supported" error.

Changes

• Strata/Languages/Python/PythonToLaurel.lean: Replace the single-target guard with a loop over all targets, calling translateAssign for each one and threading the translation context through.
• Test files: Move test_multi_assign.py and test_multiple_assign_targets.py from pending/ to the active test suite and add them to cbmc_expected.txt.

Verification

• Lean build succeeds (lake build Strata.Languages.Python.PythonToLaurel ✅)
• Full strata toIon pipeline succeeds for both test files ✅
• All existing Python tests continue to pass (VerifyPythonTest, ToLaurelTest ✅)

Fixes #890

[keyboardDrummer-bot]

The CBMC CI failure was caused by incorrect expected outcomes in cbmc_expected.txt. The two new tests (test_multi_assign.py and test_multiple_assign_targets.py) were marked as PASS but CBMC reports VERIFICATION FAILED.

Root cause: The Python-to-GOTO pipeline correctly translates the multi-assignment code, but the generated GOTO model uses uninterpreted mathematical functions (PEq, Any_to_bool, normalize_any, etc.) for the assertion checks. CBMC cannot reason about the return values of these uninterpreted functions, so it reports verification failure for any test that contains assert statements.

This is consistent with the existing tests — all tests with assertions (test_arithmetic, test_comparisons, test_control_flow, test_strings) are already marked as FAIL. The only PASS test (test_composite_return) has no assertions at all.

Fix: Changed expected outcomes from PASS to FAIL in cbmc_expected.txt (commit f934f5f).

[olivier-aws]

@keyboardDrummer-bot with this solution, it seems to me that the rhs of a multi-assignment would be evaluated multiple times. This is not correct if it has side effects, as the Python semantics is to evaluate the rhs only once and affect it then to all the lhs. Can you confirm?

[keyboardDrummer-bot]

@olivier-aws You're right. The current implementation calls translateAssign once per target, and translateAssign internally calls translateExpr ctx rhs each time (line ~1063), so the RHS expression gets translated — and would be evaluated at runtime — once per target.

In Python, a = b = f() evaluates f() exactly once and assigns the result to both a and b. The correct desugaring should be:

tmp = <rhs>
target_n = tmp
...
target_1 = tmp

(Note: Python assigns right-to-left across targets, but left-to-right within tuple unpacking.)

This is similar to the tuple unpacking pattern already in translateAssign (lines 1048–1060), which introduces a fresh temporary. I'll fix this by evaluating the RHS into a temporary variable first, then assigning that temporary to each target.

[keyboardDrummer-bot]

Good catch — I've pushed a fix in bd44966.

The multi-assignment a = b = expr is now desugared as:

multi_assign_<offset> = expr   # evaluate RHS once
a = multi_assign_<offset>      # assign temp to each target
b = multi_assign_<offset>

This follows the same temporary-variable pattern already used for tuple unpacking. The single-target case (a = expr) is short-circuited to avoid the unnecessary temporary.

Verified: lake build Strata.Languages.Python.PythonToLaurel ✅, ToLaurelTest ✅, VerifyPythonTest ✅.

[olivier-aws]

@keyboardDrummer-bot Looks great. Can you extend the tests for multi assignment to also check the case when the this has side effects?

[keyboardDrummer-bot]

Done — pushed eb86939 with a side-effect test for multi-assignment.

New test: test_multi_assign_side_effect.py uses a Counter class whose next() method increments self.count and returns it. The test does:

c: Counter = Counter()
a = b = c.next()
assert a == 1
assert b == 1
assert c.count == 1  # next() called exactly once

This would fail if the RHS were evaluated per-target (counter would be 2 for b, and c.count would be 2).

Also added an inline test in VerifyPythonTest.lean that runs the same program through the full Python → Laurel → Core → SMT pipeline.

Verified: lake build StrataTest.Languages.Python.VerifyPythonTest ✅, ToLaurelTest ✅.

[olivier-aws]

@keyboardDrummer-bot resolve git conflicts

[keyboardDrummer-bot]

Resolved the merge conflict in StrataTest/Languages/Python/VerifyPythonTest.lean. Both sides added a new test at the end of the file — our branch added the multi-assign side-effect test and main added the print() keyword arguments test. I kept both.

Pushed as commit 32d9c6e.