Audit KORE axioms

[tothtamas28]

Related:

• A modern Kore for a modern K #3306

In ModuleToKORE, a large chunk of code (as well as time executing that code) is spent generating axioms expressing certain algebraic properties of sorts and symbols. The backends then parse these axioms, and either filter them out based on the corresponding attribute without any further processing, or pattern match them to extract some information (see the K Attributes spreadsheet).

In the former case, we can just not generate the axiom. In the latter, we can introduce an attribute on the sort or symbol that encodes the desired property in a more structured and concise way.

---

Axiom	Source	Axiom attribute	Source attribute	Comment
Subsort	sort	subsort{_,_}()	none
Overload	symbol	symbol-overload{}()	none
Associativity	symbol	assoc{}()	assoc{}()
Commutativity	symbol	comm{}()	comm{}()	Not generated
Idempotency	symbol	idem{}()	idem{}()
Unit	symbol	unit{}()	unit{}()
Functional	symbol	functional{}()	functional{}()
No-confusion	symbol	constructor{}()	constructor{}()
No-junk	symbol	constructor{}()	constructor{}()
Non-executable	symbol	?	non-executable{}()?	Not generated

[Baltoli]

We should document precisely what algebraic properties we are asserting in each of these cases; there's a broader question about what KORE for rewriting vs. KORE for proving / theory is.