Add contract and transparency pass

[keyboardDrummer]

Builds on:

• Add opaque keyword to Laurel grammar strata-org/Strata#969
• Disallow transparent statement bodies #12
• Generalize multi-target assign so it supports intertwined declarations and local assignments and field assignments #22
• Enable local variables in functions strata-org/Strata#1023

No longer, maybe we can close this:

• Support functions with multiple outputs (EliminateMultipleOutputs pass) #18

Summary

Add these passes:

• [New] EliminateReturnStatements: rewrite return to exit statements, needed for the next pass.
• [New] ContractPass: translate away pre and postconditions entirely by introducing assertion and assumptions at call sites and at procedure starts and ends
• [New] TransparencyPass: for each 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 version of it, where assertions are erased and all calls are to functional versions. Tie the functional version to the procedure using a free postcondition.
• [Existing] Lift assertions, assumptions and procedure calls when they occur in expressions.
• [Follow-up] AxiomatizeExpressionAssumptionsPass: erase assumptions in Core function expressions by introducing functions and axioms.

The effect of the contract and transparency pass:

1. Allow postconditions on functions
2. Allow calling procedures from contracts
3. Improve diagnostics related to contracts, using the correct verbiage "precondition" and "postcondition" instead of "assertion"
4. Allow transparent procedures IF they have an expression body
5. Allow assertions in transparent procedures and functions

The combined effect of 2 and 4 is that there is no more difference between Laurel functions and transparent procedures.

TODO

• Differentiate between bugs and user errors in LaurelToCoreTranslator translateExpr
• Add a free postcondition to the Core procedure to tie it to its functional counterpart.
• Lift all calls inside expressions in Core procedure bodies, since they are calls to procedures and are not allowed.
• Let all remaining calls from expressions - which is all calls in Core functions, and all calls in the free procedure postconditions - be to Core functions, and other calls to procedures.
• Rename FunctionsAndProofsProgram to UnorderedCoreWithLaurelTypes and FunctionsAndProof.lean to TransparencyPass.lean

Follow-up work

• Remove the 'functional' keyword from the Laurel grammar
• Lift assumptions in expressions to axioms.
• In the transparency phase, if something has no asserts and only calls functions, only create a function and no procedure
• Move the transparency phase so its Core->Core instead of UnorderedCoreWithLaurelTypes -> UnorderedCoreWithLaurelTypes