Support transparent procedures

[keyboardDrummer-bot]

Depends on

• Formatting and debugging improvements strata-org/Strata#1115

Base PR for:

• Enable calling procedures in contracts #28

Changes

• Change handling of free postconditions in Core so they do not show up, instead of showing up as passing proofs. This is useful in this PR because this PR is adding new usages of free postconditions.
• Improve usage of source locations in the lifting phase, which improves diagnostics
• For procedure without a source body, use free postconditions instead of assuming the non-free postconditions in a generated body.
• Add the transparency pass. for each non-functional Core procedure, generate a function with the same signature and name suffixed with $asFunction. If a Core procedure is marked as transparent, attempt to generate a functional body for the $asFunction, where assertions are erased and all calls are to functional versions. Tie the functional version to the procedure using a free postcondition.
• When translating an $asFunction function to Core, do not generate Core expressions that contains assertions, such as safe division or safe destructors. In a follow-up PR, we will merge Laurel functions and procedures, with both getting both a Core function and a Core procedures, and then we will never use Core functions/expression that contain assertions.
• Refactored CoreGroupingAndOrdering to compute SCC ordering for functions and procedures separately. This is required because TransparencyPass creates a new AST type, UnorderedCoreWithLaurelTypes, where functions and procedures are already separated.

Testing

• Updated T20_TransparentBody to account for new feature. In a follow-up we will have many more tests, because we'll convert all functions in tests to procedures.
• Added T20_TransparentBodyError to capture some not supported cases