-
Notifications
You must be signed in to change notification settings - Fork 122
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Injective Fact Detection with Loop Identifier as Second Argument #627
Comments
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? |
Quoting from the manual
I think currently Tamarin only supports the first argument. |
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). |
This was never so to the best of my knowledge. 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. |
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. |
@jdreier Also happy with closing. Your call! :) Thanks for the clarification. I plan on implementing other features that supersede this anyways. |
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. |
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:
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!
The text was updated successfully, but these errors were encountered: