Remove functions

[keyboardDrummer]

Changes

1. Remove Laurel functions.
2. 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.
3. 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.
4. Improve printing of if-then-else
5. Fix contract pass so it eliminates all pre and postconditions
6. 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.
7. 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

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

[keyboardDrummer]

@keyboardDrummer-bot can you investigate the build failures? If you have trouble resolving them, just post what you found

[keyboardDrummer-bot]

I investigated the CI failure ("Build and test Lean (stable)"). Here's what I found:

Local reproduction results (with cvc5 1.3.4, matching CI):

• lake build (default targets): ✅ passes
• lake test (StrataTest build + test runner): ✅ passes (only failure is the missing ion-java-1.11.11.jar which CI downloads separately)
• StrataPython build + tests: ✅ passes
• StrataCLI build: ✅ passes
• Editor syntax verification: ✅ passes
• strata verify smoke test: ✅ passes

All of these pass from a completely clean build (deleted .lake/build first).

Most likely cause of CI failure:

The CI uses a "Restore lake cache" step that restores cached .lake directories from previous builds on the base branch (reviewed-kbd-will-merge-to-main). This PR removes the isFunctional field from the Procedure structure, which changes the serialized representation of Procedure in .olean files. If the cache restores old .olean files that contain the old Procedure layout, they would be incompatible with the new code, potentially causing deserialization failures or type mismatches during incremental builds.

Recommendation: Re-run the CI workflow. If the cache is the culprit, the CI should either:

1. Pass after the cache is invalidated by the structural change, or
2. A manual cache clear might be needed if Lake's cache key doesn't account for this kind of structural change

Note: I initially saw a BvIntCastVerifyTests failure locally, but that was because our local cvc5 was 1.2.1 which doesn't support ubv_to_int. After upgrading to cvc5 1.3.4 (matching CI), that test passes fine.

[keyboardDrummer]

I investigated the CI failure ("Build and test Lean (stable)"). Here's what I found:

Local reproduction results (with cvc5 1.3.4, matching CI):

• lake build (default targets): ✅ passes
• lake test (StrataTest build + test runner): ✅ passes (only failure is the missing ion-java-1.11.11.jar which CI downloads separately)
• StrataPython build + tests: ✅ passes
• StrataCLI build: ✅ passes
• Editor syntax verification: ✅ passes
• strata verify smoke test: ✅ passes

All of these pass from a completely clean build (deleted .lake/build first).

Most likely cause of CI failure:

The CI uses a "Restore lake cache" step that restores cached .lake directories from previous builds on the base branch (reviewed-kbd-will-merge-to-main). This PR removes the isFunctional field from the Procedure structure, which changes the serialized representation of Procedure in .olean files. If the cache restores old .olean files that contain the old Procedure layout, they would be incompatible with the new code, potentially causing deserialization failures or type mismatches during incremental builds.

Recommendation: Re-run the CI workflow. If the cache is the culprit, the CI should either:

1. Pass after the cache is invalidated by the structural change, or
2. A manual cache clear might be needed if Lake's cache key doesn't account for this kind of structural change

Note: I initially saw a BvIntCastVerifyTests failure locally, but that was because our local cvc5 was 1.2.1 which doesn't support ubv_to_int. After upgrading to cvc5 1.3.4 (matching CI), that test passes fine.

If you look at the CI results (https://github.com/strata-org/Strata/actions/runs/28098917360/job/83195378967?pr=1408), you can see that running ./run_py_interpret.sh fails. I have reproduced that locally. Please investigate these failures

[keyboardDrummer]

@keyboardDrummer-bot can you try to reproduce the SARIF failure that CI has now when running run_py_analyze_sarif.py ? https://github.com/strata-org/Strata/actions/runs/28114111319/job/83248951269?pr=1408

[keyboardDrummer]

@keyboardDrummer-bot currently the analysis if a Python test is failing. You can reproduce with ubuntu@ip-172-31-13-142:~/repos/Strata2/StrataPython/StrataPythonTest$ ./run_py_analyze.sh --filter test_bubble_sort_step. Running this command fails because it hangs. It seems like it's hanging in Core's symbolic execution step. Can you determine how the generated Core is different for this test on this PR, compared to the target branch of this PR, and think about why this causes Core to not terminate?

[keyboardDrummer-bot]

I investigated the test_bubble_sort_step hang. Here's what I found:

Root Cause: Procedure inlining causes exponential path explosion in symbolic execution

What changed between the base branch and this PR

On the base branch, the Python runtime helpers were defined as Laurel functions:

function Any_get! (dictOrList: Any, index: Any): Any { ... }
function Any_set! (dictOrList: Any, index: Any, val: Any): Any { ... }
function List_get (l : ListAny, i : int) : Any { ... }
function List_get_non_neg (l : ListAny, i : int) : Any { ... }

On the PR branch, they are Laurel procedures:

procedure Any_get! (dictOrList: Any, index: Any): Any  return ...;
procedure Any_set! (dictOrList: Any, index: Any, val: Any): Any  return ...;
procedure List_get (l : ListAny, i : int) : Any  return ...;
procedure List_get_non_neg (l : ListAny, i : int) : Any  return ...;

How this causes the hang

1. Base branch path: Any_get!(xs, 0) was a function call → translated to a Core function application (a single expression term). The SMT solver evaluates the conditional logic within function axioms efficiently.

2. PR branch path: Any_get!(xs, 0) is now a procedure call → translated to a Core call statement → in bug-finding mode, chooseEntryProceduresAndBuildInlinePhases inlines non-recursive callees into the entry procedure. Since Any_get! is not recursive, its entire body gets inlined into the test's body.

3. Any_get! has ~6 if-then-else branches (exception checks, type checks, dict vs list dispatch). Any_set! has ~7 branches. After inlining, the symbolic executor must evaluate each branch, forking execution paths at each ite with a symbolic condition.

4. The test_bubble_sort_step test has:

   • 9+ calls to Any_get! (array reads: xs[0], xs[1], xs[2] in conditions and assignments)
   • 6 calls to Any_set! (array writes: xs[0] = xs[1], xs[1] = t, etc.)

   Each inlined call adds multiple branch points. With ~15 inlined calls × ~6 branches each, the symbolic execution encounters an exponential path explosion that causes it to hang.

Why the "attempted fix" (alwaysCallCoreFunctions) is on the right track

The latest commit adds an alwaysCallCoreFunctions option that redirects calls inside procedure bodies to their $asFunction versions. This is the right direction because:

• The $asFunction versions are Core functions (not procedures)
• Function calls in Core are not inlined by the procedure inlining pass — they stay as single expression terms
• The SMT solver handles the conditional logic within function axioms without path explosion

However, the fix only redirects calls within other procedure bodies, not calls in the entry procedure itself. The entry procedure's body still calls Any_get! as a procedure, which gets inlined.

Suggested fix direction

The real fix needs to prevent path explosion when these multi-branch runtime procedures get inlined into the entry point. Options:

1. Don't inline multi-branch procedures: Modify doInlineNonRecursive to also skip procedures whose body exceeds a certain size or branch count. Then calls to Any_get! would stay as contract-inlined calls (assert pre, assume post), relying on the $asFunction postcondition for reasoning.

2. Make alwaysCallCoreFunctions apply to the entry procedure too: After inlining, redirect the remaining procedure calls in the entry body to $asFunction calls. This way, even if Any_get! starts as a procedure call, it gets redirected to a function application before symbolic execution.

3. Mark these runtime procedures with some attribute (e.g. @[no-inline] or @[prefer-function]) to prevent their inlining in bug-finding mode, keeping them as contract-based abstractions.

4. Restore these specific runtime procedures as functions: The simplest short-term fix — keep Any_get!, Any_set!, etc. as function in the Laurel runtime even though the PR eliminates functions as a language construct elsewhere.

[keyboardDrummer]

@keyboardDrummer-bot please debug the test failures:

• StrataTest.Languages.Laurel.Examples.Objects.T2c_ModifiesClausesArrayTheory
• StrataTest.Languages.Laurel.Examples.Objects.T2d_ModifiesFrameSoundness