search

DeepSec-prover / deepsec

DEciding Equivalence Properties in SECurity protocols
GNU General Public License v3.0
17 stars 2 forks source link

different treatment of public names and constants #69

Closed irakoton closed 4 years ago

irakoton commented 4 years ago

Not sure whether this behaviour is expected or not but the rewrite rules (reduc) seem to consider differently constants depending on whether they are declared with free or const.

bug.txt

If this behaviour is expected, the manual may need to be edited as it suggests that the keywords free and const are equivalent.

VincentCheval commented 4 years ago

There is a bug but not the one you're thinking.

If you declare x with free x. then x is a name meaning that it cannot appear in the rewrite rule (only constant can). As such, it is expected that reduc f(x) -> x. considers x as a fresh variable.

There is a bug however in your comment f(z) -> x, [x] would be parsed as a constant. x should be parsed as a variable and DeepSec should return an error saying that the rewrite rule is not sub term convergent.

irakoton commented 4 years ago

in the first case (free x. reduc f(x) -> x.) shouldn't we also put a warning during the parsing for example?

VincentCheval commented 4 years ago

In fact in the first case, it should have said that x is already declared as a name and that it expects a variable or a constant. It's fixed now.