Encoding stack too deep

stack.org

Encoding stack too deep

{
    let a := calldataload(0) // x1
    let b := calldataload(2) // x2
    mstore(100, 200)  // x3
    mstore(a, b)  // x4
}  

Dependencies:

Only variables

x4 depends on x1 and x2

Also side effects

x4 depends on x3

Effectively

x4 depends on x1, x2 and x3

Encoding

Dependencies are encoded by equations

$x_4 - x_1 ≥ 1$

$x_4 - x_2 ≥ 1$

$x_4 - x_3 ≥ 1$

Encoding stack too deep

Variable reference has to be at most 16 (or 17?)

$x_4 - x_1 ≤ 16$

$x_4 - x_2 ≤ 16$

Problem

1. The fact that each $x_1, \cdots, x_4$ have to be different numbers is not easy to encode.
2. SSA Variables are easier. Non-SSA assignments might be tricky.
3. Non-dependent variables may get the same value. So the final arrangement still may not be correct.

Example in z3

from z3 import Int, Optimize

x1 = Int('x1')
x2 = Int('x2')
x3 = Int('x3')
x4 = Int('x4')

cost = Int('cost')

opt = Optimize()

# Encoding non-zero constraints
opt.add(x1 >= 0)
opt.add(x2 >= 0)
opt.add(x3 >= 0)
opt.add(x4 >= 0)

# Encoding dependencies
opt.add(x4 - x1 >= 1)
opt.add(x4 - x2 >= 1)
opt.add(x4 - x3 >= 1)

# Encoding stack too deep
opt.add(x4 - x1 <= 16)
opt.add(x4 - x2 <= 16)

# cost?
opt.add(cost == x1 + x2 + x3 + x4)
# Just an invariant based on that values have to be from 1, ..., 4
opt.add(cost == 10)
h = opt.minimize(cost)
print(opt.check())
print(opt.lower(h))
print(opt.model())