Rewrite execProofMethod

[felixlinker]

This PR essentially rewrites execProofMethod and, following from that, applies some other changes. Overall, this PR should be "idempotent", i.e., Tamarin should function exactly as before. I personally find the code cleaner than before, but this is a matter of taste.

The intention behind this PR is to factor out changes to Tamarin that I did as part of a research project with @cascremers. They are necessary for that project, but we would like to check that they indeed do not change Tamarin's behavior. But still, I think that some benefit to the added clarity of the code (more deletions than insertions).

Some notes on the changes:

• I added a new proof method Finished Result that replaces Solved, Contradiction and Unfinishable. I think it makes sense to reflect in the type system which kind of methods mean that no further proving needs to be done.
• I do not check in execProofMethod whether the applied method is valid in the given constraint system. In most cases, these checks are redundant because they come from the system. Instead, I implemented checkAndExecProofMethod that is now used whenever one must check validity, e.g., upon loading a theory.
• I deleted the annotateWith(Diff)Systems functions. They performed tasks fully redundant with execProofMethod. First, you would apply a proof method and delete the resulting constraint system, then you would annotate it again.
• I now always simplify after applying a proof method. This makes the every now and then appearing "simplify" steps obsolete. To maintain backwards compatibility, I do not anymore return Nothing when simplify results in the same constraint system in execProofMethod. If I were to do that, applying a redundant simplify step (e.g., while loading older proofs) would invalidated the proof.
• execProofMethod now checks for all ways in which a proof could be finished. Therefore, applyProverAtPath need not "guess" anymore which other provers we maybe should try to apply.

Fast regression tests pass in about the same time as before on my machine. Only difference is that there are slightly fewer steps which results from the now dropped simplify steps.

I'd appreciate a thorough review and am curious about any feedback!

[felixlinker]

PS: I strongly suggest to merge by squashing and rebasing all commits. The commits themselves don't compile individually. I keep commits separate to be able to merge things back together in the end.

[cascremers]

We'll look asap, thanks!
Note the only options are "squash and merge" or "rebase and merge" -- and I presume you want the first of these.

[niklasmedinger]

Hi Felix,

thanks a lot for your work! Much appreciated.

Since I only recently got into the code base, I can't give much feedback. I'm only wondering whether execProofMethod can now be infallible because checkAndExecProofMethod exists now.

There's a small copy-paste error regarding the comments of Result. Apart from that I think the PR looks good!

[niklasmedinger]

Now that execProofMethod no longer performs any sanity checks and relies on checkAndExecProofMethod for the checks, can the return type be changed to M.Map CaseName System?

[felixlinker]

No, that doesn't work because getting the induction cases can still fail.

[niklasmedinger]

Shouldn't this be a call to checkAndExecProofMethods now that execProofMethod no longer checks whether the method is valid? Or do we rely on execProofMethod returning Nothing if the execution fails?

[felixlinker]

rankProofMethods computes all applicable methods itself, i.e., they must be valid (or the computation is buggy, but this shouldn't be fixed by checking that they are valid imo). Thus, checking whether it's valid is not necessary. At this point in the code, it cannot come from an "external" source such as a loaded proof file.

[felixlinker]

We'll look asap, thanks! Note the only options are "squash and merge" or "rebase and merge" -- and I presume you want the first of these.

I mean the first of these, yes, but technically, you could also squash commits without rebasing ☝️🤓 (Doesn't make much sense, though.)

[jdreier]

My quick merge seems not to have worked (although compilation fails on different file), I guess @felixlinker needs to help here.