Additional EVM optimizations

[PetarMax]

This PR introduces optional additional optimizations for some of the EVM opcodes. It eliminates the word stack overflow and underflow checks, relying on the hypothesis that EVM bytecode coming from Solidity will not cause a stack overflow or underflow. The speed-up on our real-world engagements ranges between 5% and 20%, as per the following tables:

	PR	master	Speedup
1	38	38	0.00%
2	30	30	0.00%
3	38	41	7.32%
4	41	43	4.65%
5	309	360	14.17%
6	460	575	20.00%
7	148	176	15.91%

	PR	master	speedup
T1	164	170	3.53%
T2	128	132	3.03%
T3	100	106	5.66%
T4	321	342	6.14%
T5	1610	1702	5.41%
T6	297	334	11.08%
T7	178	199	10.55%
T8	103	110	6.36%
T9	112	120	6.67%
T10	947	993	4.63%

[ehildenb]

Could we do this based on a cell like <stackChecks> false </stackChecks> instead of as lemma inclusion? That would allow us to turn it on/off without rekompiling, by changing the value of that cell.

[PetarMax]

Could we do this based on a cell like <stackChecks> false </stackChecks> instead of as lemma inclusion? That would allow us to turn it on/off without rekompiling, by changing the value of that cell.

Yes, we could.

[PetarMax]

Hm, but then how do I formulate these? Structurally as well, with the <stackChecks> cell? I don't think I can?

    rule #stackUnderflow(_, _) => false [priority(30)]
    rule #stackOverflow(_, _) => false [priority(30)]

[PetarMax]

I think I would like to merge this as-is. It works as intended and it's different from cell-based rules like those for <useGas> because we also override function evaluation rules. If we want to switch it on or off we do have to rekompile, but assuming that the intention behind doing so is to re-run the proofs, then we might as well rekompile. We also do not introduce further changes to the configuration and have to maintain less Python initialisation code.

[PetarMax]

It would appear that the <stackChecks> approach speeds up the execution further when stack checks are deactivated (NSC), but slows down the execution by ~3% when they are activated (SC). Data from one of the engagements:

	NSC	SC	master	NSC vs master	SC vs master
1	37	40	38	2.63%	-5.26%
2	30	31	30	0.00%	-3.33%
3	34	42	41	17.07%	-2.44%
4	38	44	43	11.63%	-2.33%
5	245	368	360	31.94%	-2.22%
6	460	587	575	20.00%	-2.09%
7	119	182	176	32.39%	-3.41%

[PetarMax]

Some interesting updates. There are essentially three version of this optimization:

1. V1: redefines stack overflow/underflow as always false, brings in a number of optimization rules. These simplifications are added at build time.
2. V2: Instead of redefining the stack overflow/underflow functions, it brings in two additional rules that override the treatment of #next so that stack overflow and underflow are never computed. Instead of adding all at build time, it introduces an additional configuration cell so that .
3. V3: V1, but with the two additional rules introduced by V3. This is what is currently in the PR.

The results on our largest real-world engagement as follows:

	V1	V2	V3	master	V1 speedup	V2 speedup	V3 speedup
T1	164	161	160	170	3.53%	5.29%	5.88%
T2	128	123	123	132	3.03%	6.82%	6.82%
T3	100	93	93	106	5.66%	12.26%	12.26%
T4	321	307	306	342	6.14%	10.23%	10.53%
T5	1610	1529	1520	1702	5.41%	10.16%	10.69%
T6	297	259	256	334	11.08%	22.46%	23.35%
T7	178	157	156	199	10.55%	21.11%	21.61%
T8	103	96	95	110	6.36%	12.73%	13.64%
T9	112	107	107	120	6.67%	10.83%	10.83%
T10	947	907	892	993	4.63%	8.66%	10.17%

and we see that V2 and V3 outperform V1, and that V3 is consistently slightly faster than V2. In addition, V2 exhibits a slowdown with respect to V1/V3 of ~3% when stack checks are turned on, probably due to the combination of an additional cell and additional high-priority rules that are always checked.

V1, given these results, is out of the picture.

The pros of the V2 approach are that we don't have to rekompile between runs of the same proof with and without stack checks. A semi-pro is that it the speed-up is comparable to V2. The cons are that we introduce a new cell into the configuration and that there is a slowdown when stack checks are turned on.

The pros of the V3 approach are that it is the fastest, and that there is no slowdown when stack checks are turned back on. The cons are that one does have to rekompile if one wants to use re-run a proof stack checks. The mitigation of that con is that our working hypothesis is strong and that we would want to re-run a proof with stack checks very rarely.

Given this data, my choice is V3. Thoughts?

[PetarMax]

We are going with V2 in the end, everything is in place and CI is passing. @ehildenb

[ehildenb]

I approved, but something to fix. When doing kontrol show ... --to-kevm-rules, it attempts to produce KEVM rules for the given KCFG that can be tested/used directly as summaries, which we have some clients using. This isn't tested very well, on CI, but changing the configuration structure of Kontrol can break it.

• In particular, here we extract the KEVM sub-configuration to produce rules runnable with KEVM, and this extraction pattern needs to be updated with the new cell.
• Second, the rules produced should not execute past rules that do not exist in KEVM, like the Kontrol cheatcodes or other instrumentation. So when new rules are added, it's good to include them in the list of rules that are done with --break-on-cheatcodes here, so that we can make sure that every time a non-KEVM rule fires we save off the node before and after. This ensures that kevm show ... --to-kevm-rules can filter out those KCFG edges (done here) which contains steps from Kontrol that aren't in KEVM.

We should also add a test of kontrol show --to-kevm-rules, because it's something that we use for another engagement. Issue here.

[PetarMax]

If these rules are included in --break-on-cheatcodes, they will make the feature completely unusable in any real-world debugging since they will fire on every #next, it’d be like --break-every-step, which simply does not scale. --break-on-chatcodes is essential for debugging the use of actual cheatcodes.

I am also not quite understanding in which context --to-kevm-rules is useful, hasn’t this been replaced by CSE? Which client would be running KEVM and not Kontrol?

All of this indicates to me that these rules should perhaps be added to KEVM (just like the <useGas> rules), not Kontrol.

[PetarMax]

I can confirm that the <stackChecks> cell gets removed with --to-kevm-rules is called.

[PetarMax]

When it comes to testing --to-kevm-rules, that feels like a job for the next PR.