Verification with NonLinear Arithmetic Disabled?

[DavePearce]

Given the known limitations of Z3, an interesting question is whether or not we can use the DafnyEVM with the flag --disable-nonlinear-arithmetic. My expectation is that this will not work out of the box. Rather, it will work once we have added lemmas in suitable places for it to verify. But, I'm not sure how much effort will be involved here. If its not too much effort ... then it might be worth doing, and maintaining going forward.

[DavePearce]

The following methods are impacted:

• function Pow(n:nat, k:nat)
• function GcdExtended(a: nat, b: nat)
• function Shr(lhs: u256, rhs: u256)
• function Div(lhs: i256, rhs: i256)
• function Rem(lhs: i256, rhs: i256)
• function Sar(lhs: i256, rhs: u256)
• function DivWithZero(lhs:u256, rhs:u256)
• function QuadraticCost(memUsedSize: nat)
• lemma QuadraticCostIsMonotonic(x: nat, y: nat)
• function f(x: nat)

Marking these with {:verify false} means that the code base with verify under --disable-nonlinear-arithmetic.