Preprocess contracts

[virgil-serbanuta]

Run the new test with

make .build/ukm-with-contract/output/endpoints.1.run.executed.kore

Fixes #120
Fixes #121
Fixes #126

[virgil-serbanuta]

This change is needed because of a K crash that does not make sense, and which looks like this:

(NoSuchElementException: key not found: inj{SortExpressionOrError{}, SortKItem{}})

These seem to be triggered by random changes in the code, not related in any way to the ExpressionOrError sort. Anyway, using explicit constructors seems to make the error go away (it may also be that this is another random code change that makes the error go away for no good reason).

[yanliu18]

It looks good to me.
The endpoint tests runs correctly in my machine.
I had a quick look at the K implementation, it seems OK to me as well.
But will still want @ACassimiro to have a look since I am new to the project.

[ACassimiro]

I may be missing something here, but wouldn't it be easier just to have a require clause specifying that signature is present in signatures? This would simplify this rule and the one above it as well.

[virgil-serbanuta]

You're right, I could have done something simpler, something like something like:

   syntax Expression ::= chooseSignature(Expression, Map, Expression, Expression)  [seqstrict(1,3,4)]
   rule chooseSignature(ptrValue(_, V:Value), SignatureToMethod, BufferId, Gas)
        => self . SignatureToMethod[Signature] (BufferId , Gas , .CallParamsList)
     requires Value in_keys(SignatureToMethod)
   rule chooseSignature(ptrValue(_, V:Value), SignatureToMethod, _, _) => :: state_hooks :: setStatus(:: ukm :: EVMC_BAD_JUMP_DESTINATION , .CallParamsList)
     requires notBool (Value in_keys(SignatureToMethod))

However, we are pretending that the "ukm::contract" macro/attribute is generating some contract struct + implementations, so it seemed more appropriate to generate exactly the same code in K.

Even so, maybe I should have went with the simpler option, given that we have a deadline, and I will do that if you think it's better. The difference between the two options did not seem to be that big to me, so I picked the one that seemed "cleaner", but that may not be the best choice.

So, should I switch to the simpler option, or should I leave the code as-is?

[ACassimiro]

I don't have any issues with leaving the code as-is, especially if, in the future, we move to a different implementation closer to the actual behavior of contract data generation.

[ACassimiro]

The implementation seems clear to me. I only have one minor comment regarding how a rule could be simplified, but I don't think that prevents this PR from being merged at all.