Attempt no. 2 at fixing rule-substitution

[goodlyrottenapple]

Fixes #3912?

There were three further issues that I identified:

• When we have a VarX in both the rule and configuration, internally they are distinguished by a different constructor. However, when externalising, this tag was lost. This PR prepends "Rule" to any rule variables and "Eq" to any Equation vars, leaving the original name for all config vars.
• After match/unification, there is some further processing before the substitution is applied. We are now capturing the simplified/normalised substitution just before it's applied and emitted in a debug message (via debugCreatedSubstitution). This should ensure that the substitution is the correct one.
• The substitution being returned contained both the mappings from rule variables to subterms of the configuration, as well as learned predicates about equalities between configuration variables and values. The latter are emitted in the rule-predicate field and should not be present in rule-substitution.

[ehildenb]

Can we add a test this time?

[geo2a]

The change looks good to me!

One question: did we run any of the downsteam projects' test suites? I'd expect the tests that use golden KoreJson files may fails as we are changing the variable names. Perhaps it's worth noting in the update deps PRs that this change needs a golden file update.

[goodlyrottenapple]

Modified this test to have a VarX both in the rule and the configuration. With this change, we get the correct rule-substitution term in the response:

{
  "tag": "Equals",
  "argSort": {
    "tag": "SortApp",
    "name": "SortInt",
    "args": []
  },
  "sort": {
    "tag": "SortApp",
    "name": "SortGeneratedTopCell",
    "args": []
  },
  "first": {
    "tag": "EVar",
    "name": "RuleVarX",
    "sort": {
      "tag": "SortApp",
      "name": "SortInt",
      "args": []
    }
  },
  "second": {
    "tag": "EVar",
    "name": "VarX",
    "sort": {
      "tag": "SortApp",
      "name": "SortInt",
      "args": []
    }
  }
}

[goodlyrottenapple]

The change looks good to me!

One question: did we run any of the downsteam projects' test suites? I'd expect the tests that use golden KoreJson files may fails as we are changing the variable names. Perhaps it's worth noting in the update deps PRs that this change needs a golden file update.

I ran the KEVM test suite and only saw one failure, however the same test failed on master, so seems unrelated