shortcircuit in forAll and And logic when operating on claim functions

[reteprelief]

At the time I wrote the Resolute documentation shortcircuit on forAll and And was disabled when used with operands that are claim functions.
A little while ago someone reintroduced the shortcircuit on forAll and And, i.e., they stop evaluating claim function calls when the first one returning false/fail is encountered. As a result, when I verify claims on a collection of buses it does not evaluate all of them unless they all return true. This behavior is like a compiler stopping after the first syntax error and not telling about the rest of them.
Shortcircuit is ok when these operators are used to call on computational functions.

[kfhoech]

A little more than one year ago @backesj changed the ResoluteProver in commits 08654d2 and eef541c such that and expressions and forall expressions had short-circuit behavior. The rationale behind this change is unclear, especially considering an explicitly short-circuited andthen operator exists. Was this possibly done for consistency between claim evaluation and function evaluation?

While I would think it strange for the language to not short circuit in claims and to do the short circuit in functions, I can understand his interest in getting all of the negative (failing) results in a claim.

Today the only difference is that the result returned in the case of the and where the left half is false the result returned is composite containing references to both the left and right results. Otherwise, the result is only the left or right result as appropriate. Thus, it affects display of the results as well as the logical result.

Even though evaluation would not be consistent, it is desirable to have both non-short-circuit (and) as well as short-circuited (andthen) operators available.

Likewise for forall expressions it is desirable in claims to evaluate and display results for all elements of the collections over which the expression evaluates.

Finally, is there likely to be the need for a short-circuited forall expression in claims. It is conceivable that a false result on one element would be a guard against evaluation of the next element. Would a forallupto be a desirable addition to the grammar?

[kfhoech]

from @agacek :
function evaluation need to short circuit to avoid exceptions and such
at the prover level, however, I can see people wanting a lot of different behavior 😕
perhaps that should be a config option (debug option: continue after failure for 'and')

[kfhoech]

I'm a little uncomfortable with a preference option. Composing a systems that are from differing authors may result in differing needs for the evaluation.
Assuming I were to change it back to the way it was, short circuit behavior is there if you want it (using andthen). But we would need to add a way of getting a short circuit forall (perhaps forallupto)?

[agacek]

The behavior only changes for failed proofs. For successful proofs, the preference option wouldn't matter. It would mainly be a debugging flag while trying to get a proof to work.

[reteprelief]

Most of the time you will have one or more proofs that fail and you will spend time to figure out what needs to be changed in the model to satisfy the proofs. Therefore it is useful to know all of the proof that fail so you know how far you are from the goal of satisfying all proofs. Only when all proofs pass you have a complete assurance case. In that case it does not matter whether we have a shortcircuit.

I am making the case that you always want the non-shortcircuit version of Forall and And when their operands are claim functions (proofs).
What are some other logic operators that make sense at that level:
"shortcircuit and": first proof is a precondition for the second proof to be performed => that led to the Andthen. In ALISA we use the keyword "then"
"implies": this is almost an "andthen" except that it also returns true if the precondition does not hold. Not very useful.
"or": Here we have the scenario that if the first proof fails or fails to complete then we want an alternative (backup) proof to be performed. In our ALISA work we are using the keyword "else".

[kfhoech]

The problem with a blanket preference option is that in some cases the author of the claim may depend upon short circuit behavior where using the left term as a guard to prevent an exception. Thus, we would want a per-claim means of selecting whether the evaluation is short circuited. I believe the best way to do this is to build it into the language.

I propose we revert the behavior for operator and to non-short-circuit when evaluating claims. The behavior for operator andthen is short circuit. For symmetry the operator or would likewise be non-short-circuit and also introduce the operator orelse for completeness. (Note this is consistent with the language convention for Ada.) Evaluation would remain short-circuit for all of these operators when evaluating functions.

Similarly, the behavior for forall would revert to non-short-circuit when evaluating claims. It is debatable whether to introduce a short-circuit version of forall (perhaps called forallupto or forallshort).

Use of exists in claims currently is disallowed. I propose this remains unchanged. UPDATE: Actually, I'm incorrect here. Exists is allowed in claims. Is there likewise a need for non-short-circuit and short-circuit versions of exists?

Comments, please?

[agacek]

Sounds good to me.

…

On Mon, Apr 16, 2018 at 9:45 AM, kfhoech ***@***.***> wrote: The problem with a blanket preference option is that in some cases the author of the claim may depend upon short circuit behavior where using the left term as a guard to prevent an exception. Thus, we would want a per-claim means of selecting whether the evaluation is short circuited. I believe the best way to do this is to build it into the language. I propose we revert the behavior for operator and to non-short-circuit when evaluating claims. The behavior for operator andthen is short circuit. For symmetry the operator or would likewise be non-short-circuit and also introduce the operator orelse for completeness. (Note this is consistent with the language convention for Ada.) Evaluation would remain short-circuit for all of these operators when evaluating functions. Similarly, the behavior for forall would revert to non-short-circuit when evaluating claims. It is debatable whether to introduce a short-circuit version of forall (perhaps called forallupto or forallshort). Use of exists in claims currently is disallowed. I propose this remains unchanged. Comments, please? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#122 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAKgiN_0i6C_wRk_9L5qpJ0BltOtNBkQks5tpK6QgaJpZM4TTpR-> .

[reteprelief]

How about disallowing implies? My problem is that it evaluates to true when the left operand is false. Often when I used it I assumed it meant "andthen".

As to a shortcut version for Forall: I am ok with not introducing it.
Typically forall is used on a collection where the order does not matter.
What we really have with a "short cut forall is a sequence of andthen, i.e., it assumes an ordering of the collection. If the order matters it tends to be different claim functions on the same object thus you do write them out and sequence them with "andthen" - the syntax becomes self-explanatory :-)

[kfhoech]

I concur with the argument that forall and exists ought to be considered as over unordered collections. Short circuiting these really does not make sense. This keeps the code cleaner and the language simpler too.

If there are models out there with forall or exists that depend on short circuit evaluation to prevent exceptions, they probably ought be refactored.

Consider the as proposal modified to remove the short-circuit versions of forall and exists. However, we would need to allow use of the list head and tail functions to enable the list destruction necessary for the refactoring, and, of course, allow recursive claim calls. Or, perhaps that ought to be delegated to functions called from the claim.

[kfhoech]

Resolved by Pull Request 126.