Help with some weird assertion behavior

[HikaruHokkyokusei]

Consider the code in this gist: https://gist.github.com/verus-play/e8994fed9bfc78602c7dc298857b549b

First, ignoring the boilerplate, the part of the code in question is from line 53-75.

Without explicit proof, Verus can assert that both maps in our states are finite.

Now, when trying to assert the expansion of system_only_accepts_one_value in temp_lemma proof, I have excluded the actual proof by using assume(false) because this code is a small reproduction of the error I was encountering, and the proof itself is not relevant.

Before assume(false), I am asserting these two statements (Line 71-72): -

assert(s.hosts[h1].accepted.dom().finite());
assert(s.hosts[h2].accepted.dom().finite());

If I don't assert them, then even after asserting the expansion of system_only_accepts_one_value in temp_lemma with assume(false) verus complains that the post condition system_only_accepts_one_value is not satisfied.

Now, since in line 60, verus is able to assert assert(all_maps_are_finite(s));, I naturally expect the above two assert statements to succeed, but verus is not able to assert them.

Any help with why this is happening?

[parno]

When I run your example, I see several recommends failures associated with the failed assertion. For example:

note: recommendation not met
  --> /playground/src/main.rs:71:20
   |
71 |             assert(s.hosts[h2].accepted.dom().finite());
   |                    ^^^^^^^^^^^
   |
  ::: /playground/verus/source/target-verus/release/vstd/seq.rs:62:18
   |
62 |             0 <= i < self.len(),
   |                  - recommendation not met

This makes sense, as in your by { } block, we don't know that h2 is in bounds. If you're trying to prove A ==> B, then in the by block, you need to add if A { // prove B }. For cases like this, where A is long and complex, you can change your assert forall to use [the implies keyword(https://verus-lang.github.io/verus/guide/reference-assert-forall-by.html?highlight=implies#assert-forall--by), instead of ==>, like this:

        assert forall |h1: int, h2: int, accept_ballot_1: nat, accept_ballot_2: nat| #![auto]
            0 <= h1 < s.hosts.len() &&
            0 <= h2 < s.hosts.len() &&
            s.hosts[h1].accepted.contains_key(accept_ballot_1) &&
            s.hosts[h2].accepted.contains_key(accept_ballot_2) implies
            s.hosts[h1].proposed_value.contains_key(accept_ballot_1) &&
            s.hosts[h2].proposed_value.contains_key(accept_ballot_2) &&
            s.hosts[h1].proposed_value[accept_ballot_1] == s.hosts[h2].proposed_value[accept_ballot_2]
        by { ... }

which automatically introduces an implicit if A { }.

[HikaruHokkyokusei]

Right. I forgot to do it in this case. I usually use implies because of the recommendation warnings. But for some reason, when I ran this code on the playground and VS Code with the analyzer extension, I didn't see the warning this time. I now found it under the problems tab in VS Code.

That said, I did replace ==> with implies. I was able to assert finiteness (which is obvious now, as it is same assuming it), but even after asserting the expansion of system_only_accepts_one_value using by assume(false), we get the error saying post-condition system_only_accepts_one_value failed.

And I do not see any other recommendations either.

[HikaruHokkyokusei]

Additionally, I just noticed that the below code works: -

proof fn temp_lemma(s_old: &System, s: &System)
requires
    inductive(s_old),
    next(s_old, s),
ensures
    system_only_accepts_one_value(s),
{
    assert(all_maps_are_finite(s));
    
    assert forall |h1: int, h2: int, accept_ballot_1: nat, accept_ballot_2: nat| #![auto]
        0 <= h1 < s.hosts.len() &&
        0 <= h2 < s.hosts.len() &&
        s.hosts[h1].accepted.contains_key(accept_ballot_1) &&
        s.hosts[h2].accepted.contains_key(accept_ballot_2) implies
        s.hosts[h1].proposed_value.contains_key(accept_ballot_1)
    by {
        assume(false);
    };
    
    assert forall |h1: int, h2: int, accept_ballot_1: nat, accept_ballot_2: nat| #![auto]
        0 <= h1 < s.hosts.len() &&
        0 <= h2 < s.hosts.len() &&
        s.hosts[h1].accepted.contains_key(accept_ballot_1) &&
        s.hosts[h2].accepted.contains_key(accept_ballot_2) implies
        s.hosts[h2].proposed_value.contains_key(accept_ballot_2)
    by {
        assume(false);
    };
    
    assert forall |h1: int, h2: int, accept_ballot_1: nat, accept_ballot_2: nat| #![auto]
        0 <= h1 < s.hosts.len() &&
        0 <= h2 < s.hosts.len() &&
        s.hosts[h1].accepted.contains_key(accept_ballot_1) &&
        s.hosts[h2].accepted.contains_key(accept_ballot_2) implies
        s.hosts[h1].proposed_value[accept_ballot_1] =~= s.hosts[h2].proposed_value[accept_ballot_2]
    by {
        assume(false);
    };
}

(No change to the rest of the code in the gist mentioned at the start of this discussion)

Was I making some logical mistake previously without realizing it? Or does it have to do something with how Verus works internally?

[parno]

This appears to be a triggering issue. You used #![auto], which appears to have chosen poorly when it comes to triggers for the quantifier in system_only_accepts_one_value. If you manually choose the first two appropriate terms (i.e., those that contain all of the quantified variables), then the proof appears to go through. In this case, I think it helps to choose the terms in the implication's antecedent.