Support Any type, Operations, and Kwargs handling for Python->Laurel by thanhnguyen-aws · Pull Request #489 · strata-org/Strata

thanhnguyen-aws · 2026-02-26T20:31:11Z

Description of changes:
This PR Any type, Operations, and Kwargs handling for Python->Laurel:

Define type Any and ListAny in PythonLaurelCorePrelude as inductive types.
Change the encoded type for all variables, functions' inputs and outputs to Any type.
Encode Python's operations in PythonLaurelCorePrelude so that they are consistent with Python's semantic.
Support Kwargs handling for Python->Laurel

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

andrewmwells-amazon · 2026-02-26T20:47:56Z

I asked Thanh to create this branch to replace #457 since I can't push to his fork

keyboardDrummer · 2026-02-27T08:49:35Z

Exciting stuff. Is the Any encoding is used for all values now? What happened to using the statically provided Python types to optimize away the Any?

andrewmwells-amazon · 2026-03-02T16:38:12Z

Exciting stuff. Is the Any encoding is used for all values now? What happened to using the statically provided Python types to optimize away the Any?

We plan to improve the partial evaluator to reduce them as much as possible. (Initial experiments suggested a 4% slowdown with this approach, which I think is worth the reduced soundness risk)

keyboardDrummer · 2026-03-02T16:55:29Z

We plan to improve the partial evaluator to reduce them as much as possible.

Until you do that, would this change mean you're able to prove less since the verification condition become more complex?

(Initial experiments suggested a 4% slowdown with this approach, which I think is worth the reduced soundness risk)

A 4% slowdown of the compilation when the partial evaluator is able to do the optimization? Are there cases where the partial evaluator won't be able to do the optimization and verification results change?

… Python->Laurel->Core with main

Strata/Languages/Python/PythonToLaurel.lean

andrewmwells-amazon · 2026-03-03T18:10:44Z

Strata/Languages/Python/PythonLaurelCorePrelude.lean

+}
+
+
+inline function PMul (v1: Any, v2: Any) : Any


There are a bunch of bugs here from copying PAdd. E.g.,
(Any..isfrom_string(v1) && Any..isfrom_string(v2)) does concat.

from_float(int_to_real(Any..as_int(v1)) + Any..as_float(v2))
uses + instead of *

I fixed them

andrewmwells-amazon · 2026-03-03T18:14:06Z

Strata/Languages/Python/PythonToLaurel.lean

-  let mut translatedArgs ← finalArgs.mapM (translateExpr ctx)
-
-  -- Check if function has a model
-  if !hasModel ctx funcName then


We want to keep this.

I added it back

andrewmwells-amazon · 2026-03-03T18:15:51Z

Strata/Languages/Python/PythonToLaurel.lean

-      | .FloorDiv _ => .ok Operation.Div  -- Python // maps to Laurel Div
-      | .Mod _ => .ok Operation.Mod
-      | .Div _ => .ok Operation.Div  -- Python / (true division)
-      | .BitAnd _ => .ok Operation.And  -- Bitwise & - abstract as logical And


We probably want to keep these

I added it back

andrewmwells-amazon · 2026-03-03T18:16:37Z

Strata/Languages/Python/PythonToLaurel.lean

-      | .LtE _ => .ok Operation.Leq
-      | .Gt _ => .ok Operation.Gt
-      | .GtE _ => .ok Operation.Geq
-      | .In _ => return mkStmtExprMd .Hole  -- Abstract: arbitrary bool (sound)


We also want to keep these

I added it back

andrewmwells-amazon · 2026-03-03T19:40:11Z

Until you do that, would this change mean you're able to prove less since the verification condition become more complex?

Yes

andrewmwells-amazon · 2026-03-03T19:49:21Z

A 4% slowdown of the compilation when the partial evaluator is able to do the optimization? Are there cases where the partial evaluator won't be able to do the optimization and verification results change?

This was timing from Core -> SMT (including solver time).

StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected

Strata/Languages/Python/PythonLaurelCorePrelude.lean

shigoel · 2026-03-03T20:29:01Z

Strata/Languages/Python/PythonLaurelCorePrelude.lean

I'd like to request comments (similar to docString style) in the prelude code below, especially since this is hand-written and has to be maintained manually, and as such, should be held to the same high standard as Lean code in this repo.

Preferably, please link to relevant Python documentation in these comments that justifies the design choices that were made.

Also, please divide the file into sections, with descriptions of what constructs/operations.. etc. are being handled in each section.

I added the documents into the prelude.

StrataTest/Languages/Python/expected_laurel/test_precondition_verification.expected

shigoel · 2026-03-04T22:19:37Z

Strata/Languages/Python/PythonLaurelCorePrelude.lean

+  if (Any..isfrom_string(v)) then !(Any..as_string!(v) == "") else
+  if (Any..isfrom_int(v)) then !(Any..as_int!(v) == 0) else
+  false
+  //WILL BE ADDED


Is this another instance of false being a placeholder value?

This function is guarded by the requires clause, so in case v is not one of the 4 types, it will returns false, but the assertion of this function will fail.

thanhnguyen-aws and others added 23 commits February 19, 2026 11:47

Add Kwargs handling

3338139

Merge branch 'main' into laureltrans

bf154d2

debugging PythonToLaural translator

d8cc1a5

using AnyTy for all vars and function signatures

79c09e5

Merge branch 'main' into laureltrans

a0409dc

add preludefunctionnames to LauralToCoreTranslator

b7e8793

fix test examples

3a74435

Add Python operations to CorePrelude + change ExceptOrNone -> Error

69e8000

Merge branch 'main' into laureltrans

7669b79

Merge branch 'main' into laureltrans

14adde6

Merge branch 'main' into laureltrans

c34879a

resolve conficts + separate CorePrelude and PythonLaurelPrelude

98cb935

Merge branch 'main' into laureltrans

afde05b

using PythonLaurelCorePrelude in Laurelanayzer

85cfbfb

fix return for null function call

b1610cb

Merge branch 'main' into laureltrans

1284933

resolve conflict

18cfb2f

fix bug

85f2804

Merge branch 'main' into laureltrans

8ab8e20

clean up PythonLaurelPrelude

8c9c030

Merge branch 'main' into laureltrans

7fd9358

change Binary operations to functions

ee689fa

Merge branch 'main' into laureltrans

6627899

thanhnguyen-aws requested a review from a team February 26, 2026 20:31

thanhnguyen-aws requested review from fabiomadge and keyboardDrummer as code owners February 26, 2026 20:31

thanhnguyen-aws added 2 commits February 27, 2026 10:53

Merge branch 'main' into laureltrans

23497a2

Merge branch 'main' into laureltrans

ff5731e

Merge branch 'main' into laureltrans

0dc6f3e

thanhnguyen-aws and others added 4 commits March 2, 2026 10:32

resolve conflicts

fea7f6e

fix pyAnalyze bug

e83d54d

fix pyAnalyze bug

1f09ea4

Disable test_field_use. Update expected test output. Clean up + merge…

bc2d178

… Python->Laurel->Core with main

andrewmwells-amazon force-pushed the laureltrans branch from 808e334 to bc2d178 Compare March 2, 2026 22:12

thanhnguyen-aws added 2 commits March 3, 2026 10:32

adding output for function call stmt

3fd344e

Merge branch 'main' into laureltrans

0ca5d1a

thanhnguyen-aws mentioned this pull request Mar 3, 2026

Python Prelude in Laurel #506

Draft

andrewmwells-amazon requested changes Mar 3, 2026

View reviewed changes

thanhnguyen-aws added 3 commits March 3, 2026 11:53

turn Any destructors to unsafe + fix Any div operator

34a29b6

fix PAdd PMul bugs

8c0365e

fix typo

36ca5ad

shigoel reviewed Mar 3, 2026

View reviewed changes

StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected Show resolved Hide resolved

shigoel reviewed Mar 3, 2026

View reviewed changes

Strata/Languages/Python/PythonLaurelCorePrelude.lean Outdated Show resolved Hide resolved

shigoel reviewed Mar 3, 2026

View reviewed changes

add BitAnd and In back

5f6cd4f

shigoel requested changes Mar 3, 2026

View reviewed changes

thanhnguyen-aws added 3 commits March 3, 2026 12:56

add back handling for missing model function calls

e9cf40f

add back req_opt_name_none_or_str for test_helper_procedure

bc3fb68

add preconditions to Any_to_bool + documentations

b659571

andrewmwells-amazon reviewed Mar 4, 2026

View reviewed changes

StrataTest/Languages/Python/expected_laurel/test_precondition_verification.expected Outdated Show resolved Hide resolved

Merge branch 'main' into laureltrans

f999465

shigoel reviewed Mar 4, 2026

View reviewed changes

thanhnguyen-aws added 2 commits March 4, 2026 15:02

Merge branch 'main' into laureltrans

8ce321e

merge with SafeDiv PR

62edd03

Conversation

thanhnguyen-aws commented Feb 26, 2026

Uh oh!

andrewmwells-amazon commented Feb 26, 2026

Uh oh!

keyboardDrummer commented Feb 27, 2026

Uh oh!

andrewmwells-amazon commented Mar 2, 2026

Uh oh!

keyboardDrummer commented Mar 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

andrewmwells-amazon commented Mar 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

andrewmwells-amazon commented Mar 3, 2026

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

keyboardDrummer commented Mar 2, 2026 •

edited

Loading

andrewmwells-amazon commented Mar 3, 2026 •

edited

Loading