HEVM: support boolean storage variables in equivalence checking

[d-xo]

Opening as a draft because I'm not quite sure what to do here, but equivalence checking currently fails for specs involving boolean storage variables. The following two should (I think) be equivalent:

contract C {
    bool b;
    function f(bool v) public {
        b = v;
    }
}

constructor of C
interface constructor()
iff CALLVALUE == 0
creates
  bool b := false

behaviour f of C
interface f(bool v)
iff CALLVALUE == 0
storage
  b => v

But are reported as non equivalent by act. I think this is because of two reasons:

1. Solidity inserts checks during abi decoding that trigger a revert if bool values in calldata are not either 0 or 1
2. Solidity masks the result of an SLoad of a bool value to ignore the top 255 bits

We currently do not account for either when running our equivalence checks in act. The first seems relatively easy to deal with by asserting that bool values in calldata are either 0 or 1 when constructing our Expr for the positive equivalence check

The second I'm not really sure what to do. The final storage expression we get from hevm is:

          (SStore
            slot:
              0
            val:
              (Or
                (IsZero
                  (IsZero
                    (Var "v")
                  )
                )
                (And
                  115792089237316195423570985008687907853269984665640564039457584007913129639680
                  (SLoad
                    slot:
                      0
                    storage:
                      (AbstractStore (SymAddr "entrypoint"))
                  )
                )
              )
          )
          (AbstractStore (SymAddr "entrypoint"))

whereas we generate:

          (SStore
            slot:
              0
            val:
              (Var "v")
          )
          (AbstractStore (SymAddr "entrypoint"))

I'm not sure what we should generate here. I also have the feeling that blindly matching the solidity semantics here might get us into trouble later down the road if we want to verify other languages...

@zoep very interested to hear your thoughts here?

[zoep]

I think the solution for this would be to respect Solidity's storage layout when compiling to hevm's Expr (and add sload masking accordingly).