Replace rule list with "DSL"

[ekpyron]

TBD

We can probably just use a triplet of Yul expressions, resp. expression patterns:

• precondition: evaluates to non-zero, if the rule can be applied
• match: pattern expression for matching the rule
• replacement: pattern expression to replace the matched code snippet

The match expression can use symbolic pattern variables for matching variables and constants and (at a later stage when extending this from expressions to statements) arbitrary code blocks. Precondition and replacement expressions can use any pattern variables used in the match expression.

[christianparpart]

@ekpyron can you give some example? (or in other words: when can we talk face-to-face about it?) I'm interested in taking this one, but I'd need some more (precise) input of what you have in mind. :)

[ekpyron]

This issue was mainly meant as a reminder to discuss this further - the idea came up with @chriseth at devcon, but I think this might need some more careful and future-proof planning before we actually start with it.

[chriseth]

Examples for potential syntax:

• //-comments are allowed everywhere.
• rules are separated by empty (non-comment) lines
• first line is match expression, second line is replacement
• we need a way to specify conditions on the dialect (EVM, wasm, hasSelfbalance, ...)
• complictated yul blocks are probably out of scope for now.
• we need a way to denote computations on constants. For simplicity of parsing, I would propose functional notation (@+)
• we should make it more obivous whether a placeholder can match anything or just literals. My proposal would be to prefix placeholders with # if they should only match literals

-EVM hasSelfbalance
// need to specify dialect, with restrictions on some rules

balance(address())
selfbalance()

//comment

add(#A, #B)
@+(A, B)

add(X, 0)
X

// rules that remove or reorder placeholders
// only match if the placeholders are movable
// This is a feature of the engine
mul(X, 0)
0

if 1 { T }
{ T }

if 0 { T }
{}

// what are the conditions on T here?
T revert(X, Y)
revert(X, Y)

// can we have "same match" on full statements?
switch X case 0 { T1... T } default { T2... T}
switch X case 0 { T1... } default { T2... } T 

[axic]

There's also #5542 as a relevant issue.

[axic]

first line is match expression, second line is replacement

If we have such a system, I think < and > prefixes would be nice (diff-style), e.g.:

< balance(address())
> selfbalance()

But @ekpyron's proposal in #5542 of defining equalities may be more intuitive:

balance(address()) == selfbalance()

[axic]

1. In this the core syntax is equality of expressions (from @ekpyron). Where there is no loss of information (replacing instructions with faster instructions, such as shifts), it could reversible too.
2. A condition can be introduced via iff <expr>. Expressions here must be "constexpr". We borrow the idea from Rust to mark these constexpr versions (macros) with exclamation mark, e.g. sub!, lt!, etc.
3. Any number of whitespace is allowed between both the rewrite rule and the condition.
4. Expressions are EVM opcodes (or yul dialect builtins).
5. Conditions are a different set of expressions/builtins. Special conditionals are introduced for wordsize, bit testing, etc.
6. The terms A, B, C mean literal on the stack, while X, Y, Z mean non-literals on the stack.
7. Properties/attributes are introduced via [@<key> <value>], eg. [@evm hasSelfbalance]. It is only valid for the following rewrite rule.
8. // marks comments.

I played with the syntax a bit and tried to translate a set of random steps from RuleList.h.

//
// Simple rules
//

[@evm hasSelfbalance]
balance(address()) == selfbalance()

exp(0, X) == iszero(X)

exp(1, X) == 1

[@evm hasBitwiseShifting]
exp(2, X) == shl(X, 1)

exp(-1, X) == sub(iszero(and(X, 1)), and(X, 1))

// move constants across subtractions
// X - A -> X + (-A)
sub(X, A) == add(X, sub!(0, A))

//
// Rules with conditions
//

//        rules.push_back({
//                Builtins::BYTE(A, Builtins::SHR(B, X)),
//                [=]() -> Pattern { return Word(0); },
//                [=] { return A.d() < B.d() / 8; }
//        });
byte(A, shr(B, X)) == 0 iff lt!(A, div!(B, 8))

//        // Replace MOD X, <power-of-two> with AND X, <power-of-two> - 1
//        for (size_t i = 0; i < Pattern::WordSize; ++i)
//        {
//                Word value = Word(1) << i;
//                rules.push_back({
//                        Builtins::MOD(X, value),
//                        [=]() -> Pattern { return Builtins::AND(X, value - 1); }
//                });
//        }
//
// In these cases it may make more sense to just expand it manually.
mod(X, 1) == and(X, 0)
mod(X, 2) == and(X, 1)
mod(X, 4) == and(X, 3)
// But could also consider adding a pseudo-variable.
mod(X, shl!(1, K)) == and(X, sub!(shl!(1, K), 1))) iff and!(gte!(K, 0), lte!(K, wordsize!()))

// Also extra whitespaces can be added for readability.
mod(X, shl!(1, K)) == and(X, sub!(shl!(1, K), 1)))
   iff
and!(
  gte!(K, 0),
  lte!(K, wordsize!())
)

//                {Builtins::SHL(A, B), [=]{
//                        if (A.d() >= Pattern::WordSize)
//                                return Word(0);
//                        return shlWorkaround(B.d(), unsigned(A.d()));
//                }},
shl(A, B) == 0 iff gte!(A, wordsize!())
shl(A, B) == shl!(A, B)

// {Builtins::LT(A, B), [=]() -> Word { return A.d() < B.d() ? 1 : 0; }},
lt(A, B) == 0 iff gte!(A, B)
lt(A, B) == 1 iff lt!(A, B)

[axic]

If we want to not have magic variable names, then as mentioned we need a way to mark literals. I think the # prefix on the match is an okay way do it, but probably makes sense to keep that prefix on both sides.

[axic]

Here are some more, line-by-line translations:

 add(#A, #B) == add!(A, B)
 mul(#A, #B) == mul!(A, B)
 byte(#A, #B) == 0 iff gte!(A, div!(wordsize!(), 8))
 byte(#A, #B) == shr!(B, and!(mul!(8, sub!(sub!(div!(wordsize!(), 8), 1), A)), 0xff)) iff lt!(A, div!(wordsize!(), 8))
 shl(#A, #B) == 0 iff gte!(A, wordsize!())
 shl(#A, #B) == shl!(A, B)
 shr(#A, #B) == 0 iff gte!(A, wordsize!())
 shr(#A, #B) == shr!(A, B)
 sub(not!(0), X) == not!(0)
 mul(X, not!(0)) == sub(0, X)
 mul(not!(0), X) == sub(0, X)
 and(X, not!(0)) == X
 and(not!(0), X) == X
 eq(X, 0) == iszero(X)
 eq(0, X) == iszero(X)
 gt(X, 0) == iszero(iszero(X))
 lt(0, X) == iszero(iszero(X))
 gt(X, not!(0)) == 0
 lt(not!(0), X) == 0
 and(byte(X, Y), 0xff) == byte(X, Y)
 byte(sub!(div!(wordsize!(), 8), 1), X) == and(X, 0xff)
 not(not(X) == X
 xor(X, xor(X, Y)) == Y
 or(not(X), X) == not!(0)
 and(and(X, Y), Y) == and(X, Y)
 mod(X, 1) == and(X, 0)
 mod(X, 2) == and(X, 1)
 mod(X, 4) == and(X, 3)
 mod(X, shl!(1, K)) == and(X, sub!(shl!(1, K), 1))) iff and!(gte!(K, 0), lte!(K, wordsize!()))
 byte(#A, shr(#B, X)) == 0 iff lt!(A, div!(B, 8))
 and(address(), sub!(shl!(1, 160), 1)) == address()
 and(caller(), sub!(shl!(1, 160), 1)) == caller()
 and(origin(), sub!(shl!(1, 160), 1)) == origin()
 and(coinbase(), sub!(shl!(1, 160), 1)) == coinbase()
 iszero(iszero(eq(X, Y))) == eq(X, Y)
 iszero(iszero(lt(X, Y))) == lt(X, Y)
 iszero(iszero(slt(X, Y))) == slt(X, Y)
 iszero(iszero(gt(X, Y))) == gt(X, Y)
 iszero(iszero(sgt(X, Y))) == sgt(X, Y)
 iszero(iszero(iszero(X))) == iszero(X)
 iszero(xor(X, Y)) == eq(X, Y)
 byte(#A, shr(#B, X)) == 0 iff lt!(A, div!(B, 8))
 sub(X, #A) == add(X, sub!(0, A))
 sub(add(X, #A), Y) == add(sub(X, Y), A)
 [@evm hasSelfbalance]
 balance(address()) == selfbalance()
 exp(0, X) == iszero(X)
 exp(1, X) == 1
 [@evm hasBitwiseShifting]
 exp(2, X) == shl(X, 1)
 exp(-1, X) == sub(iszero(and(X, 1)), and(X, 1))

[chriseth]

This looks very good! Some remarks:

• I'm not sure about the == if the two sides are not really equal (you can use lt!(#A, #B) on the RHS but not on the LHS).
• iff should be if
• maybe we should replace wordsize by bitsPerWord and bytesPerWord
• maybe use !lt instead of lt!?

Finally: Why not have

 exp(2, X) == shl(X, 1) if  evm!(hasBitwiseShifting)

instead of

 [@evm hasBitwiseShifting]
 exp(2, X) == shl(X, 1)