Remove functions by keyboardDrummer · Pull Request #1408 · strata-org/Strata

keyboardDrummer · 2026-06-24T11:44:32Z

Changes

Remove Laurel functions.
Support let expressions in transparent bodies. This is necessary to implement the above change, because the contract pass can produce let expressions when calling procedures with preconditions, and some of the updated tests have transparent bodies that call procedures with preconditions.
Fix several bugs in the lifting pass. Again this is now necessary because with more things being procedures, there were more cases where lifting had to be done correctly.
Improve printing of if-then-else
Fix contract pass so it eliminates all pre and postconditions
Verification performance is worse because calling transparent procedures has a more complicated encoding than calling functions had. Calling transparent procedures should get an encoding optimization but that's out of scope for this PR.
Added #guard_msgs (drop info) in to several tests to prevent getting info output when running lake test. These guards previously already existed but they were accidentally removed in a test refactoring.

Tests

Replaced usages of function in tests with procedure. Tests that had duplicated cases for functions and procedures had the function test-cases removed.
The T3_ControlFlow test was updated to use let expressions in a transparent body
The T2_ImpureExpressions test was updated to check for the new fixed bugs in the lifting pass
Some tests checked against printed if-then-else and they've been updated
No explicit test for this.
Updated tests. Some tests now check for "could not prove" instead of "does not hold"

…y pass

…y-pass-only

…trata into transparency-pass-only

This reverts commit d3e7594.

The function→procedure changes renumber assertion/assume IDs in the generated Core programs. Update all expected_interpret/*.expected files that had hardcoded assertion numbers to use [0-9]+ patterns instead, matching the approach already used by test_missing_models.expected.

keyboardDrummer-bot · 2026-06-29T15:25:39Z

I investigated the run_py_interpret.sh failures. The root cause is that the function→procedure changes in this PR renumber assertion/assume IDs in the generated Core programs, which breaks 16 .expected files in StrataPython/StrataPythonTest/expected_interpret/ that had hardcoded assertion numbers in their regex patterns.

For example, test_truthiness_bool_eq.expected previously matched \[ERROR\] assert $assert\(673$\) condition did not reduce to bool — but after the refactoring, the assertion is numbered differently.

Fix pushed (b46ab22): I updated all 16 affected .expected files to use [0-9]+ wildcard patterns instead of hardcoded numbers, following the same approach that test_missing_models.expected already used in this PR.

Potential remaining issues I couldn't verify (no Lean toolchain available locally):

Tests with false in .expected (e.g. test_deep_inline, test_chained_compare*) — these assume the interpreter still produces output containing "false" on assertion failure. If the function→procedure change causes these tests to fail differently (e.g. "stuck redex" instead of a clean assertion failure), these would need their .expected updated or converted to .skip files.
Tests that currently pass (no .expected file) might now fail if procedure calls don't reduce correctly in the interpreter. The alwaysCallCoreFunctions := false flag is already set for pyInterpret, so calls go directly to procedures rather than $asFunction copies.

If CI still shows failures after this push, running ./run_py_interpret.sh --update locally would regenerate all .expected files from the actual outputs.

keyboardDrummer · 2026-06-29T20:36:52Z

@keyboardDrummer-bot please investigate the CMBC failures that occur when doing ./StrataPython/StrataPythonTest/run_py_cbmc_tests.sh

keyboardDrummer-bot · 2026-06-29T20:55:53Z

I investigated the CBMC pipeline failures on this branch. Here's what I found:

Root Cause

The GOTO backend (Strata/Backends/CBMC/GOTO/LambdaToCProverGOTO.lean) only supported up to 3-argument (ternary) function applications. With this PR's change from functions to procedures, the contract pass now generates postcondition checks like test_helper_procedure$post0(arg1, arg2, ret, exception) with 4 arguments, causing:

Exception: [toGotoExprCtx] Not yet implemented: LExpr.app () (LExpr.app () (LExpr.app () (LExpr.app () (LExpr.op () { name := "test_helper_procedure$post0", ...

Affected Tests (9 tests)

All tests calling procedures with contracts failed at pyAnalyzeLaurelToGoto:

test_function_def_calls, test_class_methods, test_class_with_methods
test_datetime, test_datetime_now_tz, test_timedelta_expr
test_missing_models, test_multi_function, test_precondition_verification

Fix

I opened PR #1430 (targeting removeFunctions) that adds support for 4-6 argument function applications in both LExprT.toGotoExpr and LExpr.toGotoExprCtx. After the fix, all 29 tests in cbmc_expected.txt pass pyAnalyzeLaurelToGoto.

Additional Note

14 tests currently marked SKIP in cbmc_expected.txt now pass the pyAnalyzeLaurelToGoto stage (even without my fix — the PR's changes made them work). Their expected outcomes will need to be updated once their final CBMC verification results are determined in a full CI run with symtab2gb and cbmc.

keyboardDrummer · 2026-06-29T21:00:16Z

@keyboardDrummer-bot please cherry-pick 8a3bbe4 into this PR

The GOTO backend's toGotoExprCtx and toGotoExpr functions only handled up to ternary (3-argument) function applications. With the removal of Laurel functions in favor of procedures, the contract pass now generates pre/postcondition checks with 4+ arguments (e.g., procedure params + return value + exception variable). Add explicit pattern matching for quaternary (4), quinary (5), and senary (6) argument applications in both LExprT.toGotoExpr and LExpr.toGotoExprCtx. This fixes pyAnalyzeLaurelToGoto failures for tests that call procedures with contracts (e.g., test_helper.procedure).

keyboardDrummer · 2026-06-30T08:56:13Z

@keyboardDrummer-bot please debug the failures in this CI run: https://github.com/strata-org/Strata/actions/runs/28402459992/job/84162551771?pr=1408

symtab2gb requires the 'guard' key on every instruction, but the serializer was omitting it for non-GOTO instructions with a true guard. This caused 'instruction_from_json: key guard not found' errors for all 6 failing Python CBMC pipeline tests.

Port of GitHub PR strata-org/Strata#1408 ("Remove functions"), the StrataPythonFrontEnd half. - Convert the Laurel runtime prelude (PythonRuntimeLaurelPart) from `function` declarations to `procedure`s. - Thread `alwaysCallCoreFunctions` through PySpecPipeline / Cli. - Emit a valueless `.Return` (not a direct `$body` exit) for Python `return`, so postcondition assertions appended after the body stay reachable; pass the new `postTest` argument to `While`. Goldens: regenerated all expected_laurel/*.expected via run_py_analyze.sh --update (with label-ID normalization) and updated the test_missing_models interpret pattern. AnalyzeGoldenTest and the full FE test suite pass against the ported Strata.

…on twins Ports the TransparencyPass.lean changes from #1408: - Add redirectCallsToFunctional / redirectCallsInProc helpers - Split toUpdate into procedures needing a procedural twin vs transparent-only (via blockContainsAssumeOrAssert) - Redirect single-output twinned procedure calls to $asFunction when options.alwaysCallCoreFunctions is set - Thread LaurelTranslateOptions through createFunctionsForTransparentBodies

…ion classification Ports the coupled call-site rewrite from #1408 so that $post/$asFunction helper calls in pure contexts are no longer rejected: - Add TranslateState.procedureNames + containsProcedure, and switch the three call-site checks in translateExpr/translateStmt from the id-based model.isFunction to the name-based containsProcedure. TransparencyPass redirects foo -> foo$asFunction while preserving uniqueId, so an id-based check still resolves to the base procedure and wrongly rejects the call. - TransparencyPass: this tree still carries the isFunctional field (unlike #1408, which removes it), and the SCC/formatter/SemanticModel classification all key off it. So restore isFunctional := true on the $asFunction copies and isFunctional := false on the procedural twins, and only give a procedural twin to non-functional procedures. Without this, genuine functions (e.g. 'function assertP(x) requires P(x)') got a procedural twin, landed in procedureNames, and their calls in pure bodies were rejected. - Tests: mark 'safe' as a procedure in the Postconditions well-formedness test; update 'assertion could not be proved' -> 'assertion does not hold' in TransparentBody; regenerate the ContractPassConditionModeTest golden for the new procedure-shaped $post helpers. Full brazil-build (512 jobs) passes.

Port of GitHub PR #1408 ("Remove functions"). - Remove the Laurel `function` keyword and the `isFunctional` distinction; everything is now a `procedure`. - Support let expressions in transparent bodies (the contract pass can produce them when calling procedures with preconditions). - Fix several bugs in the lifting pass now that more constructs are procedures. - Improve printing of if-then-else (indent then/else branches). - Fix the contract pass so it eliminates all pre and postconditions. Tests: replaced `function` with `procedure` in Laurel tests (dropping duplicated function/procedure cases), updated printed-output goldens for the new if-then-else formatting and procedure encoding, and updated diagnostics that changed wording. Full StrataTest suite builds and passes.

keyboardDrummer added 30 commits May 26, 2026 09:55

Improve Laurel printer

7e34b04

Introduce transparency pass

f246686

Fixes

b11e042

Refactoring

9e4ee85

Remove pack multiple outputs pass

7408103

Add error file

4e8fa8b

Update tests

2d19629

Add sources to lift phase

c9fd151

Update tests and improve errors

19987e8

Update comment

24c3983

Trigger CI

3c23531

Trigger CI

6046381

Trigger CI

86962e4

Replace panic with safe access

d192346

Move proof skipping logic from LaurelToCore translator to transparenc…

7a04e66

…y pass

Small refactoring

a45f8f0

Merge branch 'formatting-and-debugging-improvements' into transparenc…

96b2686

…y-pass-only

Cleanup

d0fdd35

Merge branch 'transparency-pass-only' of github.com:keyboardDrummer/S…

2e0d7e1

…trata into transparency-pass-only

Add contract pass

c62cfb4

Cleanup

a95da10

Fixes

49255b4

Fixes

10640f7

Do not run the contract pass for functions yet

8c15c16

Reduce id changes

573a36b

Fixes

74ec111

Test fixes

800f6c4

Fix test

e56cb20

Fix test

a352b47

Fix test

65c92f4

keyboardDrummer added 13 commits June 29, 2026 12:11

Call procedure when interpreting

b3cac0b

Fix return in PythonToLaurel, and related things

9349000

Get rid of bodyLabel

dc8d8f4

Test updates

fce801d

More test changes

9320e88

Remove bad bodylabel reference

7205c4c

Fix modifiesClauses

07a4dab

Update tests

d149221

Update test

3c5b8c5

Fix

d3e7594

Revert "Fix"

582937b

This reverts commit d3e7594.

Fix related to holes and Core's behavior around empty procedures

d6be6e8

Fix warning

1f5b8f2

strata-org deleted a comment from keyboardDrummer-bot Jun 29, 2026

keyboardDrummer and others added 2 commits June 29, 2026 15:20

Update expect files

b1fb519

keyboardDrummer-bot mentioned this pull request Jun 29, 2026

Support 4-6 argument function applications in GOTO backend #1430

Closed

github-actions Bot added the GOTO label Jun 29, 2026

tautschnig mentioned this pull request Jul 2, 2026

JavaToLaurel: emit a procedure (not a function) for @Pure methods strata-org/jverify#461

Draft

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Remove functions#1408

Remove functions#1408
keyboardDrummer wants to merge 229 commits into
strata-org:reviewed-kbd-will-merge-to-mainfrom
keyboardDrummer:removeFunctions

keyboardDrummer commented Jun 24, 2026

Uh oh!

keyboardDrummer-bot commented Jun 29, 2026

Uh oh!

keyboardDrummer commented Jun 29, 2026

Uh oh!

keyboardDrummer-bot commented Jun 29, 2026

Uh oh!

keyboardDrummer commented Jun 29, 2026

Uh oh!

keyboardDrummer commented Jun 30, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

keyboardDrummer commented Jun 24, 2026

Changes

Tests

Uh oh!

keyboardDrummer-bot commented Jun 29, 2026

Uh oh!

keyboardDrummer commented Jun 29, 2026

Uh oh!

keyboardDrummer-bot commented Jun 29, 2026

Root Cause

Affected Tests (9 tests)

Fix

Additional Note

Uh oh!

keyboardDrummer commented Jun 29, 2026

Uh oh!

keyboardDrummer commented Jun 30, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants