Solving the second issue of PR#394 without plainOpenGoals

[yavivanov]

Hi,

As shown by PR #445, plainOpenGoals is flawed.
plainOpenGoals was introduced in #394 to fix the following problem: When Tamarin encounters a SOLVED, it should check if the given constraint system is solved. It did that by checking for open goals with the function openGoals. The problem was that openGoals is not intended for handling contradictory systems. The function is "made" for systems to which we can apply the SolveGoal ProofMethod, and its other usage is in conjunction with this method. A complete check which shows if a system is solved should also include checking if the system is contradictory. That is why replacing a "by contradiction" with a "SOLVED" in some valid proofs created "fake" proofs that Tamarin accepted. This lead to some lemmas being simultaneously verified and falsified (as shown in the minimal example). In these cases, openGoals reported no open goals, which is correct because there are no goals that can be solved by the SolveGoal method. But the systems are contradictory, and consequently, the Contradiction ProofMethod can be applied to them (they are not SOLVED). Again, openGoals can't catch this for the reasons described above.

At the same time, plainOpenGoals also falsely treats some systems, as shown by PR #445.

That is why I tried to find another solution to the problem described above.
The solution is pretty simple: when we encounter a SOLVED in a proof, we check if the constraint system is really solved by making sure that it:

1. has no open goals, i.e., the SolveGoal ProofMethod is not applicable (this is already done by openGoals)
2. is not contradictory, i.e., the Contradictions ProofMethod is not applicable (this check is introduced in this PR).

The examples from #445 and #394 behave correctly with the change. Also, the regressions tests run through with the new change.

PS: I also tested if the bug from #394 also applies to other ProofMethods, but this does not seem to be the case. OpenGoals is enough to detect if a SOLVED has been incorrectly placed in the position of another ProofMethod, but it doesn't do so for a SOLVED in the position of a contradiction method (by contradiction).

[rkunnema]

While going through old PRs, me and @kevinmorio reviewed this one again. It is still up todate with the current code base.

[jdreier]

Compilation seems to fail currently?

[jdreier]

Looks good.

Should we wait for @cascremers to review?

[cascremers]

Thanks, looking at this in the next days.

It would be great to have the minimal test cases from the other PRs too in our default regression test suite -- would it be possible to add these to the PR?

[cascremers]

@yavivanov @rkunnema @kevinmorio oops, never got round to this one. Is this still one that we need in or is this subsumed by other PRs?

If we still want it in, need to fix compilation problems.

[rkunnema]

Hi! This was only meant to be a courtesy fix for (#445) – I only wanted to report the issue! If I count correctly we are in cycle three of proposing a PR for review, months later the develop moves on and we have to merge in the new stuff ... coming from 2021.

So, please understand that I am abandoning this PR. Unless someone braver than me takes over (in, say two weeks), this PR can be closed. The issue does not seem so important.

[jdreier]

Solving the conflict was easy...

[jdreier]

For me this PR is fine, I propose to merge it if @cascremers does not object within the next week.

[cascremers]

Looking good, accepting.