[Bug] issue with is_signer

[junkil-park]

🐛 Bug

is_signer is currently implemented in the Signer module as follows:

    /// Return true only if `a` is a transaction signer. This is a spec function only available in spec.
    spec fun is_signer(addr: address): bool;

    spec module {
        axiom forall s:signer: is_signer(spec_address_of(s));
    }

It turns out that this implementation does not fit for purpose. Although the current implementation seems to be working correctly for all test cases in functional/is_signer.move, the implementation is incorrect essentially. It's the known limitation of quantifier instantiation which magically made is_signer look working. When there is no such QI limitation (e.g., when using model-based quantifier instantiation (MBQI) feature), is_signer does not work as expected.

To reproduce

Run Prover on the following module T with the config option backend.boogie_flags = ["/proverOpt:O:smt.mbqi=true"]

Code snippet to reproduce

module 0x42::T {
    use Std::Signer;
    public fun f(_s: &signer) {
        spec {
            assert exists a:address: Signer::is_signer(a);
        }
    }
    public fun f_incorrect() {
        spec {
            assert exists a:address: Signer::is_signer(a);
        }
    }
}

Stack trace/error message
Prover proves both functions although it should fail on f_incorrect. Using the option smt.mbqi=true, Prover proves f_incorrect because there exists a signer value whose address is a (see the Note section below for more information). Without the option smt.mbqi=true, Prover does not prove f_incorrect, thus looking correct.

Expected Behavior

A correct (desired) implementation should reject f_incorrect because no signer value can be found in the function.

Note

Without the config option backend.boogie_flags = ["/proverOpt:O:smt.mbqi=true"], the current implementation of is_signer seems to be working fine. However, it's working not because it's actually correct, but because the limitation of quantifier instantiation magically make it seemingly working. A simplified version of the generated boogie file is as follows:

type {:datatype} signer;
function {:constructor} signer(addr: int): signer;

function is_signer(a: int): bool;
axiom (forall s:signer :: is_signer(addr#signer(s)));

function {:inline} IsValid(s: signer): bool {
    addr#signer(s) >= 0
}

procedure f(s: signer)
{
  assume IsValid(s);
  assert (exists a:int :: a >=0 && is_signer(a));
}

procedure f_incorrect()
{
  assert (exists a:int :: a >=0 && is_signer(a));
}

Here, Boogie does not prove f_incorrect without /proverOpt:O:smt.mbqi=true, but proves it with that option.