hevm: handle contracts with boolean mappings

[d-xo]

If I attempt to prove the following spec:

constructor of Auth
interface constructor()

creates

    mapping (address => bool) wards := []

behaviour rely of Auth
interface rely(address usr)

iff

    wards[CALLER]
    CALLVALUE == 0

storage

    wards[usr] => true
    wards[CALLER]

behaviour deny of Auth
interface deny(address usr)

iff

    wards[CALLER]
    CALLVALUE == 0

storage

    wards[usr] => false
    wards[CALLER]

against this contract:

// SPDX-License-Identifier: AGPL-3.0-only
pragma solidity ^0.8.4;

contract Auth {
    mapping (address => bool) public wards;

    modifier auth {
        require(wards[msg.sender], "auth/unauthorized");
        _;
    }

    function rely(address usr) external auth {
        wards[usr] = true;
    }

    function deny(address usr) external auth {
        wards[usr] = false;
    }
}

I get the following error:

> act hevm --spec src/auth.act --soljson out/dapp.sol.json
act: "Auth_rely_wards-Auth_rely_CALLER" not found in fromList []
CallStack (from HasCallStack):
  error, called at HEVM.hs:479:28 in main:HEVM

This is because locateStorage always returns a pair of integers, even if the storage item we want to locate is a boolean type. Later when we try to lookup these storage values in SymExpBool they are stripped because they have type SymInteger instead of SymBool.

[rdotterer09]

have you already changed this in the contract or what do i need to do?