Check cell properties for restricted attributes

[Scott-Guest]

The attribute infrastructure fails to check cell properties for restricted attributes, allowing nonsense such as

configuration <myCell macro=""> .K </myCell>

[Baltoli]

We should separate out a class for attributes that can appear on configuration declarations, and do the check for these early enough to catch the sentences that are generated from these declarations.

[Baltoli]

Does the cell attribute flag the sentences we need to consider?

[Scott-Guest]

The cell attribute indeed flags Productions that come from cells. However, based on my initial attempts in #4011, we do still need to move all the attribute whitelist checks earlier in the pipeline.

Otherwise, attributes get automatically added before CheckAtt is run, and we have no way to distinguish whether they were added internally or in the actual K source code.