Adding missing base-case for exponentiation && improve Exp handling via simplification and "ite" in SMT

[msooseth]

Description

Thanks to @charles-cooper for finding a case where this gets triggered. Fixing. Anything (including 0) to the power of 0 is zero in EVM. See evm codes example

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[blishko]

LGTM!

[msooseth]

Thanks for the quick review @blishko ! Unfortunately, I'll need another review because I decided to add more fun things!

With this setup, we get:

cabal run exe:hevm -- equivalence --code-a "5b5f355f810a908060010a90805f0a906001900a5f5260205260405260605260805ff35b5b5f80fd" --code-b "5b5f358015905f526020526001604052600160605260805ff35b5b5f80fd"

Found 1 total pairs of endstates
Asking the SMT solver for 1 pairs
Reuse of previous queries was Useful in 0 cases
No discrepancies found

The corresponding SMT2 query has indeed the Exp to symbolic value:

  24   │ ;            (Exp
  25   │ ;              0
  26   │ ;              (ReadWord
  27   │ ;                idx:
  28   │ ;                  0
  29   │ ;                buf:
  30   │ ;                  (AbstractBuf "txdata")
  31   │ ;              )

and the SMT has the right ite: (define-fun buf0() Buf (writeWord (_ bv32 256) (ite (= (readWord (_ bv0 256) txdata) (_ bv0 256) ) (_ bv1 256) (_ bv0 256)) (store (store ((as const Buf) #b00000000) (_ bv95 256) (_ bv1 8)) (_ bv127 256) (_ bv1 8))))

where (ite (= (readWord (_ bv0 256) txdata) (_ bv0 256) ) (_ bv1 256) (_ bv0 256)) is the one that gets generated for the expression 0^k, in which case if k == 0 then it's 1, otherwise it's 0.

[blishko]

LGMT!