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.

[atomb]

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

[MikaelMayer]

Thorough review of the PR. The architecture is well-designed: moving definitions from Core to Laurel, SCC-based ordering for recursive functions, and the invokeOn mechanism are all clean. A few items to address below.

addressed the comments