Uniqueness of `symbol` not enforced

[tothtamas28]

kast.md defines #Top as https://github.com/runtimeverification/k/blob/01b4a3826b9c0037698efd553fcb519a0fc61b24/k-distribution/include/kframework/builtin/kast.md?plain=1#L141

and #True as https://github.com/runtimeverification/k/blob/01b4a3826b9c0037698efd553fcb519a0fc61b24/k-distribution/include/kframework/builtin/kast.md?plain=1#L143

(Similarly for #Bottom and #False.)

Both productions have the same klabel and are symbol-s. However, according to the K User Manual,

The symbol provided must be unique to this definition. This is enforced by K.

In this case, it is not enforced. As a consequence, there are productions in compiled.json that have the same klabel (field, not the attribute), which makes processing productions more difficult.

---

Possible fixes:

1. [If this is a bug] Add the missing check for symbol uniqueness. Drop #True and #False as they do not seem to be indispensable.
2. [If this is a feature] Adjust the documentation. Add a new kompiler pass that eliminates the duplicate production from compiled.json.

[Baltoli]

These are special-cased because there are multiple ways to write the symbols; this is for historical compatibility. We should be able to drop #True and #False and similar cases then make the check stricter. Possible that we rely on this somewhere, so be careful when removing cases.

Trickiest case is the empty K sequence; we are definitely using this.

[Baltoli]

There is a consensus among the K development team that we should standardise on .K as the canonical unit element of K sequences, and deprecate .. This will require a migration process for downstream code.

[Baltoli]

Blocked on actually removing . in favour of .K; that's a pretty breaking change so I want to leave warnings on for a little while before doing so. Once it's gone, we can finish removing the special-casing.

[Baltoli]

Make sure that this is atomic as a dependency update; downstream projects should be up to date before putting this through:

• EVM
• WASM + dependents (MX-*)
• MIR
• C

[Baltoli]

@tothtamas28

[Baltoli]

Take notes on what we do manually here, and then how could we automate it to help with changes of this sort in the future.

[Baltoli]

Blocked on #4066