Injective Fact Detection with Loop Identifier as Second Argument

[felixlinker]

According to @rsasse, injective facts should be detected, even if the loop identifier (fresh value) is not the first argument. This does currently not work. Here's a minimal, reproducing theory:

theory Min
begin

rule Init:
  [ Fr(~a) ] --> [ L('c', ~a) ]

rule Loop:
  [ L('c', a) ] --> [ L('c', a) ]

rule End:
  [ L('c', a) ] --> []

end

I require the loop identifier to be the second argument because the tamgiloo compiler requires the agent identifier to be the first argument 🫠

Would be good to know whether this is a bug or unsupported behavior!

[rsasse]

I may be completely misremembering what happened here, but I am reasonably sure there were versions of Tamarin that did support the injective value to be in a non-first position. Maybe @cascremers knows?

[jdreier]

Quoting from the manual

We check for each occurrence of the fact-tag in a rule that there is no other occurrence with the same first term and 1. either there is a Fr-fact of the first term as a premise 2. or there is exactly one consume fact-tag with the same first term in a premise

I think currently Tamarin only supports the first argument.

[rsasse]

Yes, but I think it was different, wasn't it? :/ Originally support for first-position, then expanded to any, but apparently that was rolled back. Or I am wrong (which is very possible).

[charlie-j]

This was never so to the best of my knowledge.
See here for the history of the relevant file: https://github.com/tamarin-prover/tamarin-prover/commits/0e1aa8f32a9cb214ff16e2a8a58fbdc5f815fa45/lib/theory/src/Theory/Tools/InjectiveFactInstances.hs

Detection was slightly improved for the subterm extension (see the relevant diff at c704b61#diff-0dd626039e62f215af8662b85ce7feff8bd91ed931122d7330b9b98e48fe1fc7), but not covering this part. What is detected at any place are monotonous counters and such things.

[rsasse]

Seems like I am misremembering in that case. Sorry!

It would be nice to support detection of injective values in any position of a fact, but for now that is not the case, and this is unsupported behavior.

So, it could of course become a feature request.

[felixlinker]

@jdreier Also happy with closing. Your call! :) Thanks for the clarification. I plan on implementing other features that supersede this anyways.

[jdreier]

Other persons have asked for the same feature, so I think this is a valid feature request, at least until this is superseded by something else.