Fix in equivalence checking

[zoep]

Description

The equivalence checker was not taking into account that an empty store is equivalent to a store with all slots initialized to zero. This was not allowing us to prove equivalence for certain smart contracts.

Summary of Changes

• If two stores are concrete and one of them is empty, the equivalence check is not performed statically (which was the case until now) but using the SMT encoding. This enforces the correct semantics
• The symExec function has now a flag that allows deployment code to be checked for equivalence
• New simplification rule (by @msooseth)
• New test that covers the problematic scenario

Closes #647.

Checklist

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

[msooseth]

Just a note to self, the issue is:

;(PEq
;  0
;  TxValue
;)
;(POr
;  (PNeg
;    (PEq
;      (ConcreteStore <empty>)
;      (ConcreteStore
;        vals:
;          (0x0,0x0)
;      )
;    )
;  )
;  (PNeg
;    (PEq
;      (ConcreteBuf
;        Length: 272 (0x110) bytes
;        0000:   60 80 60 40  52 34 80 15  60 0e 57 5f  80 fd 5b 50   `.`@R4..`.W_..[P
;        0010:   60 04 36 10  60 26 57 5f  35 60 e0 1c  80 63 87 fc   `.6.`&W_5`...c..
;        0020:   ff 0c 14 60  2a 57 5b 5f  80 fd 5b 60  40 60 04 80   ...`*W[_..[`@`..
;        0030:   36 03 81 01  90 60 3c 91  90 60 90 56  5b 60 54 56   6....`<..`.V[`TV
;        0040:   5b 60 40 51  60 4b 91 90  60 c3 56 5b  60 40 51 80   [`@Q`K..`.V[`@Q.
;        0050:   91 03 90 f3  5b 5f 60 06  90 50 91 90  50 56 5b 5f   ....[_`..P..PV[_
;        0060:   80 fd 5b 5f  81 90 50 91  90 50 56 5b  60 72 81 60   ..[_..P..PV[`r.`
;        0070:   62 56 5b 81  14 60 7b 57  5f 80 fd 5b  50 56 5b 5f   bV[..`{W_..[PV[_
;        0080:   81 35 90 50  60 8a 81 60  6b 56 5b 92  91 50 50 56   .5.P`..`kV[..PPV
;        0090:   5b 5f 60 20  82 84 03 12  15 60 a2 57  60 a1 60 5e   [_` .....`.W`.`^
;        00a0:   56 5b 5b 5f  60 ad 84 82  85 01 60 7e  56 5b 91 50   V[[_`.....`~V[.P
;        00b0:   50 92 91 50  50 56 5b 60  bd 81 60 62  56 5b 82 52   P..PPV[`..`bV[.R
;        00c0:   50 50 56 5b  5f 60 20 82  01 90 50 60  d4 5f 83 01   PPV[_` ...P`._..
;        00d0:   84 60 b6 56  5b 92 91 50  50 56 fe a2  64 69 70 66   .`.V[..PPV..dipf
;        00e0:   73 58 22 12  20 6a 9a 10  0c 51 25 bd  e2 0b 6f da   sX". j...Q%...o.
;        00f0:   fc 81 f9 f4  60 86 3e 67  61 70 b7 92  c7 03 1a b4   ....`.>gap......
;        0100:   62 6c 81 06  f7 64 73 6f  6c 63 43 00  08 1a 00 33   bl...dsolcC....3
;      )
;      (ConcreteBuf
;        Length: 272 (0x110) bytes
;        0000:   60 80 60 40  52 34 80 15  60 0e 57 5f  80 fd 5b 50   `.`@R4..`.W_..[P
;        0010:   60 04 36 10  60 26 57 5f  35 60 e0 1c  80 63 87 fc   `.6.`&W_5`...c..
;        0020:   ff 0c 14 60  2a 57 5b 5f  80 fd 5b 60  40 60 04 80   ...`*W[_..[`@`..
;        0030:   36 03 81 01  90 60 3c 91  90 60 90 56  5b 60 54 56   6....`<..`.V[`TV
;        0040:   5b 60 40 51  60 4b 91 90  60 c3 56 5b  60 40 51 80   [`@Q`K..`.V[`@Q.
;        0050:   91 03 90 f3  5b 5f 60 08  90 50 91 90  50 56 5b 5f   ....[_`..P..PV[_
;        0060:   80 fd 5b 5f  81 90 50 91  90 50 56 5b  60 72 81 60   ..[_..P..PV[`r.`
;        0070:   62 56 5b 81  14 60 7b 57  5f 80 fd 5b  50 56 5b 5f   bV[..`{W_..[PV[_
;        0080:   81 35 90 50  60 8a 81 60  6b 56 5b 92  91 50 50 56   .5.P`..`kV[..PPV
;        0090:   5b 5f 60 20  82 84 03 12  15 60 a2 57  60 a1 60 5e   [_` .....`.W`.`^
;        00a0:   56 5b 5b 5f  60 ad 84 82  85 01 60 7e  56 5b 91 50   V[[_`.....`~V[.P
;        00b0:   50 92 91 50  50 56 5b 60  bd 81 60 62  56 5b 82 52   P..PPV[`..`bV[.R
;        00c0:   50 50 56 5b  5f 60 20 82  01 90 50 60  d4 5f 83 01   PPV[_` ...P`._..
;        00d0:   84 60 b6 56  5b 92 91 50  50 56 fe a2  64 69 70 66   .`.V[..PPV..dipf
;        00e0:   73 58 22 12  20 98 6e ed  0e b0 b3 48  af 36 28 98   sX". .n....H.6(.
;        00f0:   85 39 4f 3b  15 45 6e 3e  ff 6d c5 4c  ee e7 a7 72   .9O;.En>.m.L...r
;        0100:   46 8a 92 4b  89 64 73 6f  6c 63 43 00  08 1a 00 33   F..K.dsolcC....3
;      )
;    )
;  )
;)

Where the first part of the POr is ifne, but the second is NOT equivalent -- and that's the deployed bytecode. This requires the deployed bytecode to be bit-equivalent, which is not what we want.

[msooseth]

So with some digging:

    resultsDiffer :: Expr End -> Expr End -> Prop
    resultsDiffer aEnd bEnd = case (aEnd, bEnd) of
      (Success _ _ aOut aState, Success _ _ bOut bState) ->
        case (aOut == bOut, aState == bState) of
          (True, True) -> PBool False
          (False, True) -> aOut ./= bOut
          (True, False) -> statesDiffer aState bState
          (False, False) -> statesDiffer aState bState .|| aOut ./= bOut

where (False, False) -> statesDiffer aState bState .|| aOut ./= bOut triggers.

There, aOut and bOut are actually different -- they are the concrete bytecode that gets deployed onchain, as the contract code. This is because when the init code is executed, the returndata is the final contract code. So the outputs differ, because they deploy different contracts!

NOTE: resultsDiffer is called as part of distinct which is called as part of equivalenceCheck'

[msooseth]

What we COULD do, is for such initcode we actually do two checks -- one that the state is the same after deployment (i.e. aState/bState), and that they are both Success/Failure etc. So all the above checks... except for aOut/bOut i.e. the code to be bit-equivalent. Instead, we take aOut/bOut from the success nodes, and compare them as if they were the contract being deployed, with equivalenceCheck', as normal, and an abstract starting state. That would make sure that:

• If one of them gets deployed, so does the other under the same circumstances
• Their starting state as deployed is the same (as in this case, even though they "seem" different)
• Their deployed code does the same when deployed the same way, i.e. its behaviour is the same for the same abstract starting state.

Note that SOME of the deployed code could be abstract -- the initcode could actually take parameters and place them into the aOut/bOut as symbolic values (filling in constants), though that's not the case with the simple initcode above. Thes kinds of symbolic values in the deployed contract is fine as long as it's not code, but data. The aOut/bOut will be comparable -- but we'll need what @charles-cooper has mentioned, i.e. symbolic elements of the bytecode deployed: #649

[msooseth]

Just some update. A stupid verison of this is already running. It doesn't yet deal with:

            contract C {
              uint x;
              uint private immutable CONST_NUM;
              constructor(uint k) {
                CONST_NUM = k;
              }
              function stuff(uint a) public returns (uint256) {
                unchecked {
                return (a*2)+CONST_NUM;
                }
              }
            }

where the code returned is actually partially symbolic, which is what #649 is about, but I'm making progress. It should not be too big of a deal to make that work, either. There are some things that need to be ironed out, in particular, what the return signature of equivalenceCheck should be, because there are two types of in-equivalences now: the initcode and the deployed code. For example, if one of the initcode assert-fails but the other doesn't, then it's an initcode issue. However, if the deployed codes behave differently, then it's a deployed code issue.

Anyway, for the moment, these:

            contract C {
              uint x;
              constructor() {
                x = 0;
              }
              function stuff(uint a) public returns (uint256) {
                unchecked {
                return (a*2);
                }
              }
            }

and

            contract C {
              uint x;
              function stuff(uint a) public returns (uint256) {
                unchecked {
                return (a<<1);
                }
              }
            }

are compared and are deemed equivalent -- they are checked as expected, i.e. first for initcode, and then for the deployed code.

The absolutely hideous code is at branch equiv-fix-mate. You will need eye bleach to look at it :D

[msooseth]

NOTE to self: I have a significantly improved version of this under branch equiv-fix-mate. It is not yet complete, though, as the Props of the init are not used as a precondition to the later deployed code. That's a TODO.