Compile execution constraints for optimistic precompiles

[georgwiese]

In order to get optimistic precompiles (#3366) working in practice, we need to be able to decide whether we can use the precompile already at execution time. For this, @Schaeff (in #3491) has introduced a constraint language that can be evaluated at execution time. It basically allows us to test A == B where A and B are either a constant or a tuple of (relative timestamp, register, value).

Important

As of now, #3491 can only compare entire values (looking at these datastructures). What we actually need to compare is limbs of values. That seems like a simple generalization though.

My current understanding is the following:

We want to filter both range constraints and equivalence classes for columns that are limbs of (intermediate) register values. The hope is that that filters out mostly things that the solver can derive anyway. Looking at the removed columns here, this might be the case, although it is also very common for the most significant limb of the time stamp diff to be zero, which is something that we would miss.

Finding limbs of intermediate register values can be done by looking at the memory bus interactions of the original instructions: If (1) the address space and address is constant, and (2) the data is just a list of columns (no complex expressions), we have our (relative timestamp, register, value limb) tuples. Conditions (1) and (2) would often be true I think, but e.g. in the load/store chip, it requires some solving to know which are the bus interactions that go to RAM and which go to a register.

[Schaeff]

I'm curious about supporting conditions on heap values. Basically we could extend the current Expression::Reg(Number) to Expression::Mem(Expression). In the original instructions, when we have a heap access, isn't it the case that the pointer can be expressed based on the current values of the registers?

I agree with the rest of the issue.

[georgwiese]

That would be possible, but it would be somewhat complex: The address would be something like <reg value> + <compile time offset>, but this is not trivial to infer, because the addition here is done modulo $2^{32}$. For example, the offset could be 0xffffffff (= $-1$), so there are many columns involved and the expressions would be somewhat complex.

At the same time, I don't think it's necessary, because RAM (both stack and heap) are only accessed via the mstore and mload instructions. But for those instructions, the RAM memory value is equal to a register, which I think is something the solver can infer already, so we might as well only constrain the registers.

One exception is the previous value of the RAM cell in the case of an mstore. This one is not equal to any register. But O'm not sure catching those justifies the complexity (at least in the first version).