How to turn on recommends checking in proof code?

[HaoYang670]

    spec fn is_distinct(x: int, y: int) -> bool {
        x != y
    }

    proof fn test_distinct(s: Seq<int>)
        requires
            s.len() > 0,
            forall |x: int, y: int| is_distinct(x, y) ==> is_distinct(s[x], s[y]),
    {
        assert(is_distinct(s[1], s[2]));
    }

This code could be verified. But the recommandation isn't met (0 <= x < s.len() && 0 <= y < s.len()). Is there a way to turn on the recommands,, like spec(checked)?

[utaal]

Hi @HaoYang670. This is (currently) by design: we only automatically run recommends checks on failing proofs, and there isn't, currently, a way to always enable recommends checks for non-spec functions.

For context: we are considering some changes to the recommends mechanism: for example, we will likely enable it by default for spec functions.

Can you elaborate on why you would want to check the recommends in test_distinct even when it verifies? Is it to help sanity-check your requires and ensures?

[HaoYang670]

I just want varus to warn me when I give a stronger precondition by accident (an extreme example is False).

For example it can be verify that

    proof fn test_distinct(s: Seq<int>)
        requires
            s.len() > 0,
            forall |x: int, y: int| is_distinct(x, y) ==> is_distinct(s[x], s[y]),
    {
        assert(is_distinct(s[-1], s[-2]));
    }

I know verifying precondition doesn't make sense because it is precondition. But if it breaks the recommendation, it is better to raise some warning.