ReadWord equivalence bug

[d-xo]

The result of simplifying the following expression is reported as non-equivalent by the smt solver:

(ReadWord (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) (ConcreteBuf "\163\179s\141\183\197fx\128d'Z\ETX\173\b\ESC`\v\155\141\DC3\SO\DLE\211,\237l\255g\132D\223\&6\218"))

To reproduce add the following as a top level function to test.hs and call it from the repl:

repro = do
  let p = (ReadWord (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) (ConcreteBuf "\163\179s\141\183\197fx\128d'Z\ETX\173\b\ESC`\v\155\141\DC3\SO\DLE\211,\237l\255g\132D\223\&6\218"))
  let simplified = Expr.simplify p
  print simplified
  checkEquiv simplified p

[msooseth]

Another one to trigger a variation of this:

a = (ReadWord (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) (ConcreteBuf "kkkkkkkkkkkkkkkkkkkkkkkkkkkkkkkkkkk"))
runEnv defaultEnv $ checkEquiv  a (Expr.simplify a)

This was another issue I added, accidentally. Also, another issue, #399 that is the same (marking that as duplicate:

ghci> :main -p "evalProp-equivalence-sym" --quickcheck-replay=445314 
hevm
  SimplifierTests
    evalProp-equivalence-sym: skip
[...]
Unknown
Sat (SMTCex {vars = fromList [], addrs = fromList [], buffers = fromList [(AbstractBuf "esc_LgGVZBmmiEfEmnBVPNgjyhAtrpLojASzoBhCCbpapzTjSuAsnxSoHwAuNSVW",Flat "")], store = fromList [], blockContext = fromList [], txContext = fromList []})
FAIL (5.16s)
      *** Failed! Falsified (after 47 tests):
      POr (PNeg (PLT (Lit 0x5) (And (Lit 0x38) (Lit 0x10)))) (PEq (SHA256 (CopySlice (Lit 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff) (Lit 0x4f) (Lit 0x20) (ConcreteBuf "\145@S\ESC\156\t\SI\165i\245JHx\"\221\175Z\152q\ETX\155\230\130\DEL\152\156\GS\145I\158\173\192Ma\145G\n\vH\143\211\178\FS\252\169\236E\134\198\235\234\133M\224\143\196A\205y\191\185j\170?\138\163") (AbstractBuf "esc_LgGVZBmmiEfEmnBVPNgjyhAtrpLojASzoBhCCbpapzTjSuAsnxSoHwAuNSVW"))) (Lit 0x5a))
      Use --quickcheck-replay=445314 to reproduce.

Likely culprint is 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff offset in CopySlice. Sad.

[msooseth]

(note, some version of the fix of this bug is exposable via: cabal run test -- -p '/random-contract-concrete-call/' --quickcheck-replay=146923)

Some info regarding the geth implementation:

• https://github.com/holiman/uint256/blob/master/uint256.go#L162
• https://github.com/ethereum/go-ethereum/blob/bc6d184872889224480cf9df58b0539b210ffa9e/core/vm/instructions.go#L495
• https://github.com/ethereum/go-ethereum/blob/bc6d184872889224480cf9df58b0539b210ffa9e/core/vm/interpreter.go#204

func calcMemSize64WithUint(off *uint256.Int, length64 uint64) (uint64, bool)

func memoryMLoad(stack *Stack) (uint64, bool) {

And:

func (in *EVMInterpreter) Run(contract *Contract, input []byte, readOnly bool) (ret []byte, err error) {
[...]
			if operation.memorySize != nil {
[see code here]

Together mean that geth simply does NOT define what happens with large memory offsets. Its definition of what happens with large offsets is 100% fully dependent on gas when offset is large. The execution phase of geth is essentially undefined/incorrect(?) when offset is >64b.

One fix we discussed is to limit memory to 64b. I think 32b would make more sense. But either way, it's not easy, I think. My thoughts:

• CopySlice & "ReadWord+WriteWord combo" rewrites would need to take into account that the offset wraps around.
• Perhaps some other rewrites would also need to be adjusted
• Long-term easy-to-support setup would be to have a new e.g. Lit64b (or Lit32b). But that would make a mess of Expr because now we have two types of Lit. Otherwise it may be easy to miss a wraparound check in our rewrites.

[d-xo]

One potential approach would be to change the type of Buf in the smt encoding from (define-sort Buf () (Array Word256 Byte)) to (define-sort Buf () (Array Word64 Byte)) and then just truncate the input index of readWord down to a 64 bit word. This would probably be a perf optimization at the smt level, but might open up a whole new can of words related to wrapping semantics here.

In general I'm actually quite ok with modifying our fuzzers to not generate this kind of annoying edge case and leaving this as a known issue for now. It's a rather uninteresting edge case, and one that seems extremely hard to fix. A cex in this particular case will always represent a false positive (because a write to memory at this index will always be unexecutable in the real world due to gas overflow), so having a very good and correct semantics at this edge case brings us basically nothing. As a final point, since geth doesn't define a behaviour here, it's not really possible for us to be unsound in this case since the real semantics (geth) actually doesn't proscribe a correct behaviour.

[blishko]

Apparently, evmtool does not implement wrap-around semantics.
Trying to deal with this at the SMT level (prevent the wrap-around semantics, which is natural for SMT bit-vectors) would require too much effort and would unnecessary complicate the encoding.
It is not worth it given that such cases should not occur in the real-world contracts.

The fuzzer has been modified to not generate such expressions: #598.