Simplify exponentiation in SMT backend #106
Conversation
IMO, specs should conform to "mathematical rigor", and not so much evm details, meaning I think we should ideally disallow specs which admit division by zero as part of future spec validity checking (discussed at #14). |
| -- Returns `Nothing` if the expression contains symbols. | ||
| eval :: Exp a -> Maybe a | ||
| eval e = case e of | ||
| And a b -> [a' && b' | a' <- eval a, b' <- eval b] |
There was a problem hiding this comment.
monad comprehension! Cool, haven't seen this before
There was a problem hiding this comment.
In lieu of idiom brackets you take what you can get :)
Ok so following that reasoning we want to truncate downwards instead of towards zero, since that's how Euclidean division works. Then the code here should be correct. |
Closes #99, i.e. we can now pass any exponentiation where the exponent is concrete to the SMT backend even though it has no support for exponentiation. This does not however include any algebraic analysis to attempt to simplify away symbolic values.
I'm a bit uncertain on how division is to be dealt with. Currently I'm using
divandmodfrom Haskell's Prelude (rather thanquotandrem). This is because they truncate towards negative infinity, which is what the EVM seems to be doing according to the yellow paper. But what exactly are we trying to agree with? The EVM? In that casex/0should be0, so we need a special case for that. Or Solidity? Or our other backends?