Integers & Bitvectors in Act and bytecode verifying backends

[MrChico]

Every arithmetic expression in an act Behaviour is a true integer expression, and can therefore never overflow or underflow. This makes it easier to express and prove interesting, higher level properties and in mosts cases for developers to accurately capture intended meaning of smart contracts.

However, since the EVM is always dealing with words instead of integers, there are currently two problems arising from this discrepancy:

1. There are things expressible in act that cannot be implemented in the EVM. If we specify that a storage location changes:

x => x + a

the RHS of the rewrite can be larger than 2^256 and for it to be at all possible for a contract to realize this spec we must further assume x + a. It would be reasonable to add a stage to the act compiler which checks if an overflow is possible for every subexpression in a behaviour, and warn the user if that is the case. Expressions that are topmost terms on the left hand side of a mod should be exempt from this check.

2. Since the current hevm symbolic implementation deals with bitvectors instead of integers, all act claims have to be translated into bitvectors, which turns out to be quite detrimental for proving any spec containing safemath.

The bottleneck here is in the integer - bitvector conversion in the smt solver. A fairly trivial looking claim like this:

(declare-fun a () (_ BitVec 256))
(declare-fun b () (_ BitVec 256))
(define-fun max () Int 115792089237316195423570985008687907853269984665640564039457584007913129639935)
(define-fun aNat () Int (bv2nat a))
(define-fun bNat () Int (bv2nat b))

(assert (< (+ aNat bNat) max))

(assert (not (= (bvadd a b) ((_ int2bv 256) (+ aNat bNat)))))

(check-sat)

is too difficult for z3 and cvc4 to resolve in a reasonable timeframe.

It appears that the only solution right now to make the hevm backend act compatible is to implement to follow KEVM's suit and implement the EVM logic in terms of integers modulo 2^256 instead of bitvectors of size 256.