Adding annotation reuse results in non-termination of that lemma

[hxenia]

I noticed, that adding the lemma annotation "reuse" to a lemma resulted in non-termination of that lemma.
Here is a minimal theory:

`theory test

begin

rule Start:
[ Fr(~n)]
--[ Begin(~n)
, End(~n) ]->
[ End(~n) ]

lemma NonTerminationWithReuse[reuse]:
"All #i a. End(a)@i ==> Ex #j. End(a)@j"

lemma false:
"All a #i. End(a)@i ==> F"

end`

When the lemma annotation "reuse" is omitted, the lemma NonTerminationWithReuse is proven automatically. With the annotation "reuse", the simplification step results in an infinite loop.

An observation: The non-termination does not occur when the second lemma is removed or it is trivially true.

I tested this with the latest develop version, compiled today.

[cascremers]

Hi, I don't have a machine at hand, but my conjecture is that adding the reuse annotation does not at all affect the termination of the annotated lemma. What is a more likely (and possible) explanation is that the reuse annotation means that the second lemma ("false") reuses the first one when the tag is present. Thus, depending on the presence of the annotation in the first lemma, the expansion of the second lemma changes. This can influence the termination (or precomputation) for the second lemma. This would also be consistent with your observation regarding the presence of the second lemma. You can probably test this quickest by running your file in the interactive mode, and try to autoprove separately. Alternatively, you can try to prove only the first lemma using the command-line options, though this may be a bit harder to tell apart in case it's the precomputation that is looping. Could you please check this? If my conjecture is correct, it's not a bug, but it would still be interesting to understand which part of the second lemma loops (precomputation or, more likely, proof construction). Best, Cas

…

On Tue, Jun 27, 2023 at 5:11 PM Xenia ***@***.***> wrote: I noticed, that adding the lemma annotation "reuse" to a lemma resulted in non-termination of that lemma. Here is a minimal theory: `theory test begin rule Start: [ Fr(~n)] --[ Begin(~n) , End(~n) ]-> [ End(~n) ] lemma NonTerminationWithReuse[reuse]: "All #i a. ***@***.*** <https://github.com/i> ==> Ex #j. ***@***.*** <https://github.com/j>" lemma false: "All a #i. ***@***.*** <https://github.com/i> ==> F" end` When the lemma annotation "reuse" is omitted, the lemma NonTerminationWithReuse is proven automatically. With the annotation "reuse", the simplification step results in an infinite loop. An observation: The non-termination does not occur when the second lemma is removed or it is trivially true. I tested this with the latest develop version, compiled today. — Reply to this email directly, view it on GitHub <#558>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AALJWOCKT6DKBW4VKPKYV2TXNLZ3JANCNFSM6AAAAAAZVYDOIU> . You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[hxenia]

Hi Cas,

Thanks for your quick response.

Yes, that is the behaviour that I would also expect. However, the non-termination occurs for the first lemma. Here step by step what I did:

1. Start Tamarin in interactive mode and open theory
2. click on sorry of first lemma (NonTerminationWithReuse): I immediately get the proof methods on the right side.
3. click simplify: the UI is loading, the terminal seems to be looping over splitEqs and End

However, I can also produce the behaviour that you describe: when I click on sorry on the second lemma (false) I get the same looping behaviour during the precomputation, so the proof methods on the right do not load in the UI.

When removing the reuse form the first lemma, the first lemma can be proven with auto and the second one can be disproven as well.

In the process of creating a minimal example, I also encountered this loop later in the proof process of the first lemma.

Best,
Xenia

[cascremers]

Ok, this needs a bit more investigation then. Nevertheless, it seems to depend on the presence of the second lemma, so the issue is not just local to the specific lemma.

[hxenia]

Here is a longer example theory, where this looping occures in the 4th proof step. Maybe that provides some more insights.

theory test

begin

builtins: multiset

rule Start:
    [ Fr(~n), Fr(~id)]
  --[ Begin(~n, ~id)
    , Loop(~n, ~id) ]->
    [ Loop(~n, ~id) ]

rule Loop:
    [ Loop(a, id), Fr(~n) ]
  --[ Loop(~n, id) ]->
    [ Loop(~n + a, id) ]

lemma LoophasToStart[use_induction,reuse]:
  "All #i a id. Loop(a, id)@i ==> Ex #j b. Begin(b, id)@j"

 lemma dummy:
   "All a id #i. Loop(a, id)@i ==> F"

end