Simplification With Semantic Equality

[msooseth]

This rule doesn't seem to type-check in simplify:

    go o@(Div (Mul a b) c)
      | a == c = ITE (eq a (Lit 0)) (Lit 0) b
      | b == c = ITE (eq b (Lit 0)) (Lit 0) a
      | otherwise = o

Error:

Couldn't match type ‘'End’ with ‘'EWord’
  Expected: Expr a1
    Actual: Expr 'End

Which is I think because Div is

  Div            :: Expr EWord -> Expr EWord -> Expr EWord

but ITE is:

  ITE            :: Expr EWord -> Expr End -> Expr End -> Expr End

Probably I'd need some type restriction on rule? Maybe I'll try to discuss this in person.

Not an important thing.

[msooseth]

Just to document some of our discussion here -- this does not work because ITE can only be at toplevel. Forgot that. Also, some restricted version of this could be added, with exact check against Lit 0, however, that would not be a semantic check, so it would not be as general as the ITE version. It may be worthwhile removing the restriction of toplevel-only-ITE, but we'll see.

[d-xo]

In general I think what is desired here is to extend our simplification engine to allow for checking semantic equality (not just syntactic equality as currently works). One potential way to do this would be to start calling out to an smt solver during simplification.

[msooseth]

I think I'm closing this, because I realized that (a*b)/b is actually not necessarily a anyway, due to overflow. Regarding calling out to the SMT during simplification is I think a good idea, and I think should be done as part of https://github.com/ethereum/hevm/issues/331.