feat: conservatively abstract unsupported Python constructs

[MikaelMayer]

What

Instead of failing on unsupported Python constructs, translate them to sound over-approximations so the verifier can still run.

How

Construct	Abstraction
Unsupported expressions	Hole (fresh uninterpreted value)
Unsupported binary operators	Hole
Compound LHS assignment (a[i]=v, (a,b)=v)	Havoc all in-scope variables (aliasing may affect any of them)
Tuple unpacking in for (for a,b in ...)	Havoc all target names
with statement	Body translated; as-targets declared as Hole
Unsupported statements	Havoc all in-scope variables + assert *

Unsupported statements and compound LHS assignments are recorded in TranslationContext.abstractedStatements and emitted as warnings by pyAnalyzeLaurel.

Tests

Added test_with_statement.py.

[olivier-aws]

As a general comment, I'm not a big fan of hiding away what we don't support. There are many risks of unsoundness with this. At the very least, we need a message in the log that the translation encountered an unsupported expression/statement and over-approximated it.

[olivier-aws]

I'm not sure this is sound in Python, due to aliasing. This Python script prints 999:

a = [1, 2, 3]
b = a
b[0] = 999
print(a[0])

Here you would only havoc b, not a

[MikaelMayer]

Indeed good catch. The answer there is that we should havoc not just all name targets but all names in scope.

I hadn't reviewed that part yet but I'm happy you did!

[MikaelMayer]

On a second thought, if we stored dictionaries via an indirection to the heap, then no target would be havoc-ed, we would here only havoc the heap to indicate something changed, so we would still be able to prove a[0] == b[0]
What is the status of the heap in Laurel? Is it fully supported?

[ssomayyajula]

AFAIK Laurel does allow arbitrary StmtExprs to occur on the LHS of an assignment, it's just that Laurel->Core only supports assignmets to identifiers https://github.com/strata-org/Strata/blob/main/Strata/Languages/Laurel/LaurelToCoreTranslator.lean#L362 (that is, Laurel supports heap-parameterized procedures + the creation of objects of composite type on the heap, but not assigning to their fields after the fact)

[keyboardDrummer]

(that is, Laurel supports heap-parameterized procedures + the creation of objects of composite type on the heap, but not assigning to their fields after the fact)

What? You can assign to fields whenever you like: https://github.com/strata-org/Strata/blob/main/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean#L40

I would prefer to change the field selector syntax from # to . but I ran into some technical issues. Will resolve them at some point.

[MikaelMayer]

Agreed. The unsupported statement catch-all now records the abstraction in ctx.abstractedStatements and emits a warning via pyAnalyzeLaurel. Unsupported expressions also record warnings via the ExprM monad.

[joehendrix]

Is this dropping "warnings"?

[MikaelMayer]

Yes and it should not. Thanks for spotting.

[MikaelMayer]

Fixed: translateDictKWords, translateVarKwargs, translateKwargs, and translateCall now use ExprM so warnings from nested expression translations are propagated rather than dropped. translateStmt also uses translateExprW for condition/value expressions to merge warnings into ctx.abstractedStatements.

[MikaelMayer]

The core idea of abstracting unsupported constructs to sound over-approximations instead of failing is good. The ExprM monad for accumulating warnings and the havoc-all-vars + assert-star pattern for unsupported statements are well-designed.

However, there is a bug that makes the warning mechanism non-functional for the main body: at line 1758 of PythonToLaurel.lean, pythonToLaurel' returns ctx instead of finalCtx, so all abstractedStatements accumulated during translateStmtList are lost. The pyAnalyzeLaurel caller will never see any warnings. Fix: return (program, finalCtx). I verified this compiles cleanly.

Additionally, translateAssign uses translateExprVal which silently drops expression warnings, creating an inconsistency with how translateStmt handles them.

The PR description mentions compound LHS assignment and tuple unpacking in for as abstracted constructs, but neither is implemented — both still throw unsupportedConstruct. The catch-all at the end of translateStmt only catches unmatched statement types, not sub-cases within already-matched statements like For or Assign. The description also claims test_with_statement.py was added, but it's not in the diff (it was added in PR #580).

I'd like the bug fixed and the PR description corrected before approving.