Configuration blocks in spthy files and a new default oraclename

[yavivanov]

Hi!

This PR introduces two new features.

1. Configuration blocks in spthy files. It adapts the approach from PR Request for comments: configuration within spthy #220 to the newest Tamarin version and, in particular, the refactored Parser and the new TheoryLoader. The parsing approach itself is due to @kelnage. I implemented the configuration block as a new TheoryItem, so that it fits better with all other parts of a theory (e.g. this eases printing it).

2. The default oraclename is changed to theory_filename.oracle. This is achieved by saving the filename of the theory in a field of the parsed theory. In this way, it can be used later to create the default oraclename (if the default oracle is needed).

The PR also adds two new regression tests (one for each feature).
I added them to the Makefile and the python script. Note that I added them to the fast examples (because they only need a fraction of a second each). The configuration block test is, additionally, a part of the feature tests.

Of course, the PR passes the regression tests.

[cascremers]

Thanks! Two questions:

Q: Would it be possible to break this PR into two? It seems there are two very different things going on.

Q: Does this mean that if a user has an oracle with the old name, and updates Tamarin to develop, their current setup stops working?
If this is the case, I think it would be preferable from a user's perspective to check for the old name too, and use that as a fallback (possibly with a warning), otherwise we will probably get a lot of questions on the mailing list, and possibly waste users' time.

[yavivanov]

Hi,

Thanks! Two questions:

Q: Would it be possible to break this PR into two? It seems there are two very different things going on.

Q1: Yes. The two ideas are disjoint, and so is their code.

Q: Does this mean that if a user has an oracle with the old name, and updates Tamarin to develop, their current setup stops working? If this is the case, I think it would be preferable from a user's perspective to check for the old name too, and use that as a fallback (possibly with a warning), otherwise we will probably get a lot of questions on the mailing list, and possibly waste users' time.

Q2: It only affects users that rely on the default oraclename being "oracle" (the old default).
The following scenario captures these cases:
We have an author that wrote a theory (example.spthy). They named the oracle for it "oracle". Let's say that the author relies on the default oraclename being "oracle".
They have set the global theory heuristic or some lemma heuristic to "o" without specifying an oraclename. They also don't specify an oraclename in the command line.
Thus, as no oraclename was specified, Tamarin would default to "example.oracle" when proving "example.spthy" (instead of "oracle" as it does now). So, it would raise a "non-existent file or directory" error.
I did not find occurrences of these cases in the example collection.

But "oracle" was the default oraclename for a long time, so a form of backward compatibility makes sense.

[rkunnema]

Q: Would it be possible to break this PR into two? It seems there are two very different things going on.
Q1: Yes. The two ideas are disjoint, and so is their code.

Well, there is a connection and I think a good reason for the two to be in the same PR. The goal of this PR is to transfer the information about how to properly call the theory into the .spthy file. Currently, this information in the Makefile (or sometimes in external READMEs, depending). We want to simplify benchmarks in the future.

Doing this raises the question how to specify which oracle script to use. We discussed the security implications of letting the .spthy file invoking script in the original PR. Here's a link to the last comment in the thread.

#220 (comment)

Q2: Does this mean that if a user has an oracle with the old name, and updates Tamarin to develop, their current setup stops working?

This is for setups outside our repository, right? Yes, I think falling back to oracle and giving a warning is the right way of dealing with this. @yavivanov would this feature be hard to add?

[yavivanov]

This is for setups outside our repository, right? Yes, I think falling back to oracle and giving a warning is the right way of dealing with this. @yavivanov would this feature be hard to add?

I think that it is easy to implement. It's just one additional "does the file exist?" check, and this is easily done in Haskell.

[rkunnema]

Awesome, feel free to go ahead with that, then.

[cascremers]

Yes, that would be great. We should try to ensure backwards compatibility where possible.

…

On Mon, Nov 28, 2022 at 8:51 AM rkunnema ***@***.***> wrote: Awesome, feel free to go ahead with that, then. — Reply to this email directly, view it on GitHub <#512 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AALJWOHACD56PUTA5IM2RUDWKRP6VANCNFSM6AAAAAASKUBHDM> . You are receiving this because you commented.Message ID: ***@***.***>

[rkunnema]

1832c1c adds the backward requested compatability feature. The checks pass. @kevinmorio will write the documentation in the manual. Once that PR is ready, I will hit merge on both. (So let me know if you have objections.)

[jdreier]

Would it be possible to also adapt regressionTest.py to make sure it also compares the configuration block?

[kevinmorio]

The PR for the manual: tamarin-prover/manual#118.

[rkunnema]

@yavivanov my quick and dirty merge failed, I will need your help there.

[yavivanov]

@yavivanov my quick and dirty merge failed, I will need your help there.

I'm looking into it 👍🏻

[yavivanov]

@yavivanov my quick and dirty merge failed, I will need your help there.

The above commit fixes the errors.

[rkunnema]

Thanks @yavivanov ! I think we are good to merge now. I'll wait until end of the week in case somebody has another request.