Fix #697, improve handling of precondition obligations

[joscoh]

Issue #, if available: #697

Description of changes:
When generating function precondition proof obligations, Strata Core now:

• Short circuits by generating assumptions from boolean operators (not just "implies" as previously)
• Handles let-bindings lazily, including assumptions. This means that e.g. let x := 3 / 0 in true generates no proof obligations, and let x := 3 / 0 in true || (x > 0) generates a trivial one.

Includes unit tests in PreconditionsTests.lean and a short-circuiting example in FunctionPreconditions.lean.

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

[MikaelMayer]

Well-designed PR. The lazy let-binding semantics and short-circuit assumption propagation are cleanly implemented. The test coverage is thorough, covering ||, &&, ==>, unused let-bound variables, nested lets with body calls, and the bvar shifting logic. A few minor observations below.

[MikaelMayer]

Here is my last assessment and recommendation of the situation.
I think we should not have Core expressions (even with preconditions) creating proof obligations. Core expressions are always total and so are Core functions. The precondition mechanism we have is a way to only specify what the value of a function is if the precondition is satisfied, but we already assign an uninterpreted value if the precondition is not satisfied. So there is no error introduction.

This also means that the phase that removes function preconditions to introduce proof obligations should be done in the part of the pipeline where it's ok to consider preconditions as errors semantically, and where it's possible to insert assertions directly just before the function call. That part seems to be most likely Laurel, which combines statements and expressions seamlessly.

I know that Core leverages these function preconditions in at least two places now: division by zero, datatype destructor ability. Both define two operators functions, one with preconditions and one without.
The problem is that the semantics of Core currently does not trigger errors or assertions on failing preconditions, so the path forward is to either go full mode and accept that expressions can fail, and that should be reflected in the semantics, so that we can prove the soundness of these potential failures when eliminating function preconditions; or my now slightly preferred that we move all these precondition checks to Laurel which is more suited than Core to do a small transformation that eliminate the function preconditions.

You can dismiss my review if others are convinced otherwise, but I think we are all in a state right now where we aren't sure of the current path we are taking, so I wanted to write down my own thoughts.

[joscoh]

Agree with Mikael that more discussion about the semantics is needed. Marking as a draft for now until we discuss.

[keyboardDrummer]

Hey, I'm not sure I follow all the details in the discussion, but still I think that

function A(): Bool
function B(): Bool requires A

const x := if A() then B() else false

should behave the same as:

function A(): Bool
function B(): Bool requires A

const x := A() && B()

And currently that's not the case for Core.

Would it be possible to only include the first part of this PR, Short circuits by generating assumptions from boolean operators (not just "implies" as previously), @MikaelMayer ?

A resolution of this issue is blocking the correct implementation of short-circuiting && and || in Laurel, which we need to replace Dafny for JVerify.