Record Solidity/K mapping for input names

[palinatolmach]

Partially addresses #710.

As suggested by @ehildenb, this PR generates a new file out/kompiled/input-mapping.json that contains a mapping between a Solidity variable name and its K representation. The file is structured as follows:

    "lib%forge-std%src%interfaces%IERC20": {
        "allowance(address,address)": {
            "VV0_owner_114b9705": "owner",
            "VV1_spender_114b9705": "spender"
        },
        "approve(address,uint256)": {
            "VV0_spender_114b9705": "spender",
            "VV1_amount_114b9705": "amount"
        },
    },

This PR also changes the return value of arg_names from a list of processed input names to a dictionary storing a mapping between the processed (VV0_from_114b9705) and original (from) input names.

This mapping is then used to decode K variable names back to the original ones in the mode/counterexample, which depends on these two PRs in KEVM and pyk:

• kevm: Add variable_name_mapping to print_model, print_failure_info evm-semantics#2560
• pyk: Add variable_names_mapping to APRProof, counterexample generation k#4574

For our documentation CounterTest example, the model looks like this:

  Model:
    x = 12648430
    block.number = 0
    tx.origin = 10
    msg.sender = 10
    block.timestamp = 0
    inLuck = 1

It can also be useful when parsing precondition NatSpec comments (WIP), and for Simbolik. The newly generated file doesn't occupy too much additional storage: it takes 256 Kb on a relatively big client codebase, where contracts.k takes 2.6 Mb.

[palinatolmach]

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