Add variable_names_mapping to APRProof, counterexample generation

[palinatolmach]

Related to runtimeverification/kontrol#747.

This PR adds an additional field variable_name_mapping to APRProof. The field is supposed to store a dictionary that is generated during kontrol build, which stores a mapping between the K representation (VV0_from_114b9705) and original (from) function input names. This mapping is needed to translate variable names back from a K representation during model/counterexample generation.

Generally, we only need it when computing proof.failure_info, but I couldn't find a better way to propagate this mapping info there, other than adding it to APRProof. The dictionary only contains several globally accessible variables (block.timestamp, etc.) and inputs to the specific proof, so it shouldn't take up much space when serialized.

A mapping that will be generated in Kontrol looks like this:

    "VV0_owner_114b9705": "owner",
    "VV1_spender_114b9705": "spender"
    ...

[ehildenb]

This seems too specific to store in APRProof, could it instead be stored in the Foundry object in Kontrol directly?

[palinatolmach]

As suggested by @ehildenb, the better approach would be to allow semantics to customize failure info and counterexample printing, in a manner similar to node printing:

• k/pyk/src/pyk/proof/show.py

  Line 55 in 85c8bcb

  def __init__(self, kprint: KPrint, node_printer: NodePrinter | None = None):

• https://github.com/runtimeverification/evm-semantics/blob/fcf947e1d530d608d87bfdc8c86144e6fd2c3466/kevm-pyk/src/kevm_pyk/kevm.py#L636
• https://github.com/runtimeverification/kontrol/blob/9043d62a039d2e9954d2e6b131788fc850725546/src/kontrol/foundry.py#L1365

[palinatolmach]

Closing as stale. Will implement it in a new PR.