feat(python): Add support for ** (power) operator by MikaelMayer · Pull Request #690 · strata-org/Strata

MikaelMayer · 2026-03-27T16:49:17Z

The Python-to-Laurel pipeline rejected programs using the ** operator with "Binary operator not yet supported: Pow", causing an exit-4 crash.

This PR adds support by:

Mapping Pow to the existing PPow prelude function in PythonToLaurel.lean
Constant-folding ** with integer literal operands at translation time (e.g. 1024 ** 3 becomes 1073741824)
For non-constant operands, PPow delegates to an uninterpreted int_pow function, handling int×int, bool×int, and int×bool combinations
Replacing the PPow stub (which threw UnimplementedError) with the real implementation

Tested with a new test_power.py test that verifies 8 ** 2 == 64 and 2 ** 10 == 1024 through the full pipeline. Existing tests pass.

The Python-to-Laurel pipeline rejected programs using the ** operator with 'Binary operator not yet supported: Pow'. Add support by: - Mapping Pow to the PPow prelude function in PythonToLaurel - Constant-folding ** with integer literal operands at translation time - For non-constant operands, PPow delegates to an uninterpreted int_pow function, handling int*int, bool*int, and int*bool combinations - Replacing the PPow stub with a real implementation Add test_power.py verifying 8**2==64 and 2**10==1024 through the full pipeline.

Strata/Languages/Python/PythonLaurelCorePrelude.lean

joehendrix

I added a question above, but we could postpone that for a later commit.

Strata/Languages/Python/PythonLaurelCorePrelude.lean

Strata/Languages/Python/PythonToLaurel.lean

MikaelMayer · 2026-03-27T17:15:15Z

Re: moving constant folding to concreteEval — investigated this. The issue is that int_pow must be declared in the prelude (so PPow can reference it), but adding a factory function with the same name causes a "function already exists" error during evaluation (addFactoryFunc rejects duplicates). For now, constant folding stays in PythonToLaurel for literal operands. Moving it to concreteEval would require allowing factory functions to override/merge with prelude declarations.

Moving concreteEval to PyFactory causes duplicate-name errors since int_pow must be declared in the prelude for PPow to reference it, and addFactoryFunc rejects duplicates. Revert PyFactory changes and restore constant folding in PythonToLaurel for literal operands.

MikaelMayer · 2026-03-27T17:57:22Z

Re: moving constant folding to concreteEval — investigated this. The issue is that int_pow must be declared in the prelude (so PPow can reference it), but adding a factory function with the same name causes a "function already exists" error during evaluation (addFactoryFunc rejects duplicates). For now, constant folding stays in PythonToLaurel for literal operands. Moving it to concreteEval would require allowing factory functions to override/merge with prelude declarations.

We did that for regular expressions, please check the PR that introduced them. Regular expressions are core functions that were exposed in Laurel, we should do the same.

External Laurel functions (bodyless declarations) are still translated to Core, unlike re_fullmatch_str which is filtered by the Laurel-to-Core translator. Adding int_pow to the factory causes duplicate-name errors. Constant folding for literal Pow operands stays in PythonToLaurel.

MikaelMayer · 2026-03-27T18:00:57Z

Investigated the regex pattern. The difference is that re_fullmatch_str (returning regex type) is filtered out by the Laurel-to-Core translator, so it never reaches Core's addFactoryFunc. But int_pow (returning int) IS translated to Core as a bodyless function, causing a duplicate when the factory also provides it.

To use concreteEval for int_pow, we'd need to either:

Filter int_pow in the Laurel-to-Core translator (like regex functions)
Allow addFactoryFunc to merge/override bodyless declarations

Both are larger changes. For now, constant folding for literal ** operands is done in PythonToLaurel. Non-constant cases use the uninterpreted int_pow from the prelude.

MikaelMayer · 2026-03-27T22:44:36Z

Investigated the regex pattern. The difference is that re_fullmatch_str (returning regex type) is filtered out by the Laurel-to-Core translator, so it never reaches Core's addFactoryFunc. But int_pow (returning int) IS translated to Core as a bodyless function, causing a duplicate when the factory also provides it.

To use concreteEval for int_pow, we'd need to either:

Filter int_pow in the Laurel-to-Core translator (like regex functions)

Allow addFactoryFunc to merge/override bodyless declarations

Both are larger changes. For now, constant folding for literal ** operands is done in PythonToLaurel. Non-constant cases use the uninterpreted int_pow from the prelude.

What do you mean re_fullmatch_str is filtered out by the Laurel to Core translator? There is an equivalent in Core's factory and I'm sure that the Laurel gets mapped to the Core equivalent, it was done recently in a PR that even has some tests to prove it (including PR 615 that proves that regex support works)
IF it's a matter of having different names you can do this.

The problem of doing constant folding in PythonToLaurel is that it's outside of Core. It's better if all the transformations remain in Core, including constant folding that can be done during partial evaluation of Core.
So figure out a way. We shouldn't need to merge or override bodiless declarations.

Move constant folding for ** from PythonToLaurel to a factory function (intPowFunc) in PyFactory.lean with concreteEval. This follows the same pattern as regex factory functions. To avoid duplicate-name errors when the prelude declares int_pow and the factory also provides it, ProgramEval now skips bodyless functions that already exist in the factory (the factory version has concreteEval).

MikaelMayer · 2026-03-27T22:50:20Z

Moved constant folding to concreteEval in PyFactory.lean (intPowFunc). To resolve the duplicate-name issue, ProgramEval now skips bodyless functions that already exist in the factory — the factory version with concreteEval takes precedence. This follows the regex factory pattern.

Strata/Languages/Core/ProgramEval.lean

…aurel The regex pattern (factory concreteEval) works because re_fullmatch_str uses the regex type which doesn't exist in Core, so the function is naturally filtered during Laurel-to-Core translation. int_pow uses int which translates fine to Core, causing duplicate-name conflicts with the factory. Constant folding for literal ** operands stays in PythonToLaurel. Non-constant ** produces PPow which throws UnimplementedError (same as before this PR, but now the pipeline doesn't crash on Pow).

MikaelMayer · 2026-03-30T13:01:33Z

Reverted the ProgramEval hack. Investigated why regex works: re_fullmatch_str uses the regex type which doesn't exist in Core, so the Laurel-to-Core translator naturally filters it out (fails in handleUnaryOps). The factory then provides it without conflict.

int_pow uses int which translates fine to Core, causing the duplicate. Constant folding for literal ** operands stays in PythonToLaurel. To move it to concreteEval, we'd need a mechanism to prevent specific prelude functions from being translated to Core.

Forward-declare int_pow before CoreOnlyDelimiter (like re_fullmatch_str) so the DDM parser resolves it but it doesn't enter the Core program. The factory provides int_pow with concreteEval for constant folding. Remove constant folding from PythonToLaurel and ProgramEval hack.

MikaelMayer · 2026-03-30T14:55:40Z

Moved int_pow to factory concreteEval following the regex pattern. Forward-declared before CoreOnlyDelimiter (like re_fullmatch_str) so it doesn't enter the Core program. Factory provides it with concreteEval. Removed constant folding from PythonToLaurel and the ProgramEval hack.

The native binary filters prelude checks, producing 5 results instead of 27. Update expected file to match CI output.

Strata/Languages/Python/PythonLaurelCorePrelude.lean

When exp < 0, Python returns a float (e.g. 2**-3 = 0.125). PPow now returns from_float(float_pow(...)) for negative exponents. float_pow is an uninterpreted function (forward-declared before CoreOnlyDelimiter, provided by factory). Bool exponents don't need the guard since bool_to_int returns 0 or 1.

joscoh · 2026-03-30T18:47:37Z

Strata/Languages/Python/PyFactory.lean

+
+-- Float exponentiation (uninterpreted). Used for negative integer exponents
+-- where Python returns a float (e.g. 2 ** -3 = 0.125).
+def floatPowFunc : LFunc Core.CoreLParams :=


Not completely sound, e.g. 3^(-1) is not representable as a float, but this is as good as we can do until we have proper float support, I believe.

Mmmh in general no but in python it is. So perhaps something we will do in the future is to rename these functions so that we know they correspond to a certain implementation. Integers are unbounded ,but floats are bounded.

I'm confused why this being Python makes a difference? Floats are always bounded

joehendrix · 2026-03-30T19:03:03Z

Strata/Languages/Python/PythonLaurelCorePrelude.lean

+  else if (Any..isfrom_int(v1) && Any..isfrom_bool(v2)) then
+    from_int(int_pow(Any..as_int!(v1), bool_to_int(Any..as_bool!(v2))))
+  else
+    exception(UndefinedError ("Operand Type is not defined"))


What about the following to reflect we are mssing a few cases (like float and operator overloading).

Suggested change

exception(UndefinedError ("Operand Type is not defined"))

exception(UnimplementedError("Pow is not defined on these input types"))

Applied the suggestion — changed to UnimplementedError.

joehendrix

I added a couple comments, but don't consider them blocking.

joehendrix · 2026-03-30T19:04:25Z

StrataTest/Languages/Python/tests/test_power.py

+    assert x == 64, "8 ** 2 should be 64"
+
+    y: int = 2 ** 10
+    assert y == 1024, "2 ** 10 should be 1024"


It'd be good to cover special cases (bool, negative exponents, maybe float if supported).

Added bool base cases (True5, False3). Negative exponents return from_float(float_pow(...)) which is uninterpreted — can't assert on the result in a test, but the path is exercised. Float base operands fall through to UnimplementedError.

Per review feedback: float operands and operator overloading are not yet supported, so UnimplementedError is more accurate than UndefinedError.

Cover True**5 and False**3 per review feedback. Negative exponents and float operands are handled but can't be asserted on in tests (results are uninterpreted or exceptions).

MikaelMayer added 2 commits March 27, 2026 16:48

Merge branch 'main' into feat/python-pow-operator

48fd4ad

MikaelMayer marked this pull request as ready for review March 27, 2026 16:57

MikaelMayer requested a review from a team March 27, 2026 16:57

joehendrix reviewed Mar 27, 2026

View reviewed changes

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

joehendrix previously approved these changes Mar 27, 2026

View reviewed changes

joscoh reviewed Mar 27, 2026

View reviewed changes

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

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

MikaelMayer dismissed joehendrix’s stale review via 4c0e1d5 March 27, 2026 17:15

Merge branch 'main' into feat/python-pow-operator

a03ea0f

MikaelMayer added 7 commits March 27, 2026 18:01

Merge branch 'main' into feat/python-pow-operator

1dc7acf

Merge branch 'main' into feat/python-pow-operator

e5eaba1

Merge branch 'main' into feat/python-pow-operator

20e0d3d

Merge branch 'main' into feat/python-pow-operator

c656fe1

Merge branch 'main' into feat/python-pow-operator

8ec8145

Merge branch 'main' into feat/python-pow-operator

87ab351

Merge branch 'main' into feat/python-pow-operator

7da7302

Merge branch 'main' into feat/python-pow-operator

77e624b

MikaelMayer commented Mar 30, 2026

View reviewed changes

Strata/Languages/Core/ProgramEval.lean Outdated Show resolved Hide resolved

joscoh added the Python label Mar 30, 2026

MikaelMayer added 4 commits March 30, 2026 16:17

fix: Update test_power expected output to match native binary

7180e09

The native binary filters prelude checks, producing 5 results instead of 27. Update expected file to match CI output.

Merge branch 'main' into feat/python-pow-operator

94ef9f8

Merge branch 'main' into feat/python-pow-operator

27e971f

Merge main into feat/python-pow-operator

4d3eb3d

MikaelMayer commented Mar 30, 2026

View reviewed changes

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

MikaelMayer marked this pull request as draft March 30, 2026 18:16

MikaelMayer marked this pull request as ready for review March 30, 2026 18:37

joscoh previously approved these changes Mar 30, 2026

View reviewed changes

Merge branch 'main' into feat/python-pow-operator

0d5c775

joehendrix reviewed Mar 30, 2026

View reviewed changes

joehendrix previously approved these changes Mar 30, 2026

View reviewed changes

fix: Use UnimplementedError for unsupported Pow input types

71a403c

Per review feedback: float operands and operator overloading are not yet supported, so UnimplementedError is more accurate than UndefinedError.

MikaelMayer dismissed stale reviews from joehendrix and joscoh via 71a403c March 30, 2026 19:13

test: Add bool base cases to test_power

cd7e2dd

Cover True**5 and False**3 per review feedback. Negative exponents and float operands are handled but can't be asserted on in tests (results are uninterpreted or exceptions).

	exception(UndefinedError ("Operand Type is not defined"))
	exception(UnimplementedError("Pow is not defined on these input types"))

Conversation

MikaelMayer commented Mar 27, 2026

Uh oh!

Uh oh!

joehendrix left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

MikaelMayer commented Mar 27, 2026

Uh oh!

MikaelMayer commented Mar 27, 2026

Uh oh!

MikaelMayer commented Mar 27, 2026

Uh oh!

MikaelMayer commented Mar 27, 2026

Uh oh!

MikaelMayer commented Mar 27, 2026

Uh oh!

Uh oh!

MikaelMayer commented Mar 30, 2026

Uh oh!

MikaelMayer commented Mar 30, 2026

Uh oh!

Uh oh!

joscoh Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

MikaelMayer Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

joscoh Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

joehendrix Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

MikaelMayer Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

joehendrix left a comment

Choose a reason for hiding this comment

Uh oh!

joehendrix Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

MikaelMayer Mar 30, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

joehendrix left a comment •

edited

Loading