Resolve Laurel in Python pipeline

[keyboardDrummer]

Note: it would be possible to extract the Laurel changes in this PR, the top 5 bullets, into a separate PR. They're also easy to review in isolation though since they only affect files in Laurel folders.

Changes

Laurel

• Change grammar for if/then/else in Laurel to match that of Core expressions (but not statements) and Lean. { and } is now only for blocks
• Add an optional invokeOn property to Laurel procedures, which acts like a Verus broadcast and creates an axiom for the procedure's postcondition
• Support (mutually)recursive Laurel functions
• Add support for constrained types to Laurel's Resolution phase
• Report Laurel resolution errors on the incoming Laurel program, before the Laurel->Laurel transformations, instead of after.

Python

• Move almost all definitions from PythonLaurelCorePrelude to PythonRuntimeLaurelPart
• In the Python pipeline, let all non-rec Laurel functions use the inline attribute when translating to Core
• Turn on Laurel resolution error reporting in the Python pipeline

Caveats

• Core currently requires all recursive functions to specify a cases argument. Laurel will simply use the first datatype argument as the cases argument, which could be incorrect. In a future PR, I will use the decreases clauses from Laurel to determine the cases argument. Initially, we will only support a decreases clause that contains just a single datatype parameter, because of the restrictions of Core.

• Currently, Core library/factory functions need to have their signature be redefined in a Laurel prelude file, which creates some duplication. In a future PR, we should enable Laurel to automatically import these Core functions. Example of the code duplication:

function re_pattern_error(s: string): Error
  external;

function Str.InRegEx(s: string, r: Core regex): bool external;

• PythonLaurelCorePrelude.lean still exists, because it contains two functions that have a signature with function types, that Laurel can't express yet. I will enable and move those functions in a follow-up PR.

Testing

• Tests updated for new if/then/else grammar
• Added a test-file for invokeOn
• Added a test file for recursive Laurel functions

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

[MikaelMayer]

Solid PR that moves a large chunk of the Python runtime prelude from Core to Laurel, adds invokeOn, recursive functions, and constrained type resolution. The CoreGroupingAndOrdering.lean module is well-structured with clear docstrings. A few items to address below.

[atomb]

I suggested two small changes, and two comments (thanks to Kiro) that could potentially lead to more substantive changes.

[atomb]

Is this bug documented somewhere?

[atomb]

Kiro gives me more on this:

AndThen/OrElse are now translated to non-short-circuit boolAndOp/boolOrOp:

| .AndThen => return binOp boolAndOp
| .OrElse => return binOp boolOrOp

The Laurel AST explicitly documents these as short-circuit operators ("Short-circuit logical conjunction. Only evaluates the second argument if the first is true."). The previous ite-based translation preserved short-circuit semantics. The new translation evaluates both operands unconditionally, which is a semantic change. The T15_ShortCircuit.lean test now marks several previously-passing assertions as expected failures with // TODO caused by a bug in Core. — this confirms the regression. If this is intentional (trading short-circuit correctness for simplicity while a Core-level fix is pending), the TODO comments should be more specific about what the Core bug is and link to a tracking issue.

[joscoh]

Is this bug documented somewhere?

Created issue #697 (it was on my TODO list already)

[keyboardDrummer]

Linked to the issue

[atomb]

Kiro says:

Instance procedure bodies are now unconditionally replaced with .Opaque [] .none []:

instanceProcedures := instanceProcedures.push { proc with body := .Opaque [] .none [] }

This discards the translated method body. The comment at line 1615 says "Laurel does not yet support instance procedures, so treat them as if they were static", but the body erasure means any postconditions from the method are also lost. If this is intentional (methods are treated as abstract stubs), it should be documented more explicitly.

[keyboardDrummer]

Before this PR those methods were skipped entirely, not just the body. Now they're included to prevent resolution errors, but without a body. I've added a TODO now