Immutable variables can't be made symbolic

[palinatolmach]

As brought up by @lucasmt, immutable variables are getting inlined in runtime bytecode of the contract and are not actually placed in storage. This means that they aren't

• symbolicStorage doesn't affect them, since they are not actually in storage. This means that if we want them to be symbolic we need to pass the symbolic value to the constructor, which probably means the bytecode of the contract will have symbolic variables in the middle, and it's unclear if that's supported correctly;
• they can't be accessed by the load and store cheatcodes.

The first step towards supporting immutable variables is to allow assigning them symbolic values through the constructor. However, as described in runtimeverification/evm-semantics#2219, that causes issues in #computeValidJumpDests.

[palinatolmach]

We did some investigation, and it looks like

• there is dedicated bytecode around the immutables
• location of immutable variables in the bytecode is also available in solc-generated artifacts as immutableReferences

"evm.deployedBytecode.immutableReferences - Map from AST ids to bytecode ranges that reference immutables"

Then, once the location is confirmed, symbolic values should be put there for those variables that are not initialised explicitly.

Running a constructor with symbolic parameters leads to an error @RaoulSchaffranek reported previously in runtimeverification/evm-semantics#2219: it fails in #computeValidJumpDests.

In addition, this lemma suggested by @PetarMax helped simplify a byte accessing expression:

    // Byte indexing in terms of #asWord
    rule BA [ X ] => #asWord ( #range (BA, X, 1) )
      requires X <=Int lengthBytes(BA)
      [simplification(40)]

[palinatolmach]

@ovatman @yale-vinson let's start with this item first (instead of #458) since it's needed for the engagement.

[ovatman]

I've spend some time working on this issue. Here are some remarks:

• It may not make much sense to support immutables without supporting symbolic values in constructors.
• This PR by @RaoulSchaffranek together with the lemma mentioned in the PR's discussion resolved symoblic arguments in constructors in my local tests.
• I've also performed performance tests following this approach. Attaching performance test results below. On average PR even performs better but kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k test times out on booster when run with the PR.

Legacy for the files below I've used the tags before/after to indicate the results before the PR is applied and after the PR is applied

compare_booster.txt
compare_legacy.txt

[palinatolmach]

Related: runtimeverification/evm-semantics#2219

[palinatolmach]

Closed as completed by #596, allowing immutable variables to be made symbolic through constructor arguments.