Reject definitions with constructor inconsistencies

[ttuegel]

Following #709, we realized there are other misuses of constructors which we should reject. Some of these will also need to be addressed in the frontend.

• Reject constructors with variable result sorts.
• Reject axioms with \equals between different constructors.

[ana-pantilie]

We're not sure what "Reject constructors with variable result sorts." means. Does it mean that we should identify when 2 constructors have the same name but different sorts, or should we not accept constructors which have a sort variable as the result sort?

@ehildenb or @dwightguth or @virgil-serbanuta what do you think?

[ana-pantilie]

We're not sure what "Reject constructors with variable result sorts." means. Does it mean that we should identify when 2 constructors have the same name but different sorts, or should we not accept constructors which have a sort variable as the result sort?

@ehildenb or @dwightguth or @virgil-serbanuta what do you think?

[ana-pantilie]

f [function]

rule f(x) => c requires a ==K b

\implies(a ==K b, \equals(f(x), c))

rule a #Equals b => #Top
\implies(requires, \equals(lhs, rhs /\ ensures))

if lhs, rhs or ensures = \bottom, then

\implies(requires, \bottom)

if requires = \top, then the result is \bottom

Suggestion: add a check to kore-check-functions which simplifies the lhs, rhs and ensures of all equations in the definition, and throws an error if any of them is \\bottom; this means that the definition is potentially inconsistent

[ana-pantilie]

Related to runtimeverification/k#2135

[virgil-serbanuta]

Huh, that's interesting.

I don't know what Tom meant, but I think that there should be no constructors having a pure variable as a result, because that variable may be concretized to a hooked sort, which is undesirable. Also, this is related to the original concern of the PR he mentioned.

Having the same name for a constructor for two sorts should also not be possible, but then it should probably be impossible to have a symbol with two sorts in general (in the kore language, not in k). I'm assuming that the backend already checks for that, but, if it doesn't, I wonder what would happen if someone tried to use such a symbol.

There is a third class, when a constructor's sort is parameterized, but i guess that should be fine as long as the sort's parameters are also parameters of the symbol.

[ana-pantilie]

Makes sense, thank you @virgil-serbanuta !