Unused lemma significantly slows down verification

[matthias-brun]

The text below is something I wrote for my thesis. It's an example where simply having a lemma present in the context (but unused) causes verification to slow down a lot. I'm using this as an example of how simply changing the context can have a significant impact on Z3's performance.

But it occurred to me that this may actually be a bug in either Verus or Z3. Maybe related to the triggering weirdness reported in #306?

The text below are the instructions to reproduce that behavior. It likely also happens on newer Verus commits but I haven't checked.
$VNRK_PATH refers to the path where the verified-nrkernel repo is.

We use Verus at commit 5356d52, the verified-nrkernel repository at
the newest commit on the branch timeout-lemma (https://github.com/utaal/verified-nrkernel/tree/timeout_lemma) and Z3 version 4.10.1.

We first run the command

$RUST_VERIFY --time --arch-word-bits 64
  --verify-module pt_impl::l1
  $VNRK_PATH/page-table/main.rs

and observe the following output:

verification results:: verified: 50 errors: 0
total-time:           37246 ms
    rust-time:             2544 ms
        init-and-types:        1458 ms
        lifetime-time:         1086 ms
        compile-time:             0 ms
    vir-time:               427 ms
        rust-to-vir:             82 ms
        verify:                 336 ms
        erase:                    3 ms
    air-time:              1266 ms
    smt-time:             33004 ms
        smt-init:                 0 ms
        smt-run:              33004 ms

Then we delete lines 43--48 in the file page-table/pt_impl/l1.rs, which should
be the following ones:

#[verifier(external_body)]
proof fn slow_down_everything()
    ensures
        forall|d: Directory, base: nat, pte: PageTableEntry|
               d.inv() && #[trigger] d.accepted_mapping(base, pte) ==>
               d.interp().accepted_mapping(base, pte);

Then we rerun the previous command and observe that the verification time is much shorter:

verification results:: verified: 50 errors: 0
total-time:           18637 ms
    rust-time:             2526 ms
        init-and-types:        1445 ms
        lifetime-time:         1081 ms
        compile-time:             0 ms
    vir-time:               399 ms
        rust-to-vir:             87 ms
        verify:                 302 ms
        erase:                    3 ms
    air-time:              1240 ms
    smt-time:             14466 ms
        smt-init:                 0 ms
        smt-run:              14466 ms

The single largest contributor to the changed verification time is a specific function. With the
following command we verify just that one function.

$RUST_VERIFY --time --arch-word-bits 64
  --verify-module pt_impl::l1
  --verify-function Directory::lemma_interp_of_entries_disjoint
  $VNRK_PATH/page-table/main.rs

With lines 43--48 present, we see the following output:

verification results:: verified: 3 errors: 0
total-time:           21466 ms
    rust-time:             2567 ms
        init-and-types:        1481 ms
        lifetime-time:         1086 ms
        compile-time:             0 ms
    vir-time:               288 ms
        rust-to-vir:             83 ms
        verify:                 196 ms
        erase:                    2 ms
    air-time:               382 ms
    smt-time:             18224 ms
        smt-init:                 0 ms
        smt-run:              18224 ms

With the lines removed, we see this output:

verification results:: verified: 3 errors: 0
total-time:            5844 ms
    rust-time:             2555 ms
        init-and-types:        1474 ms
        lifetime-time:         1081 ms
        compile-time:             0 ms
    vir-time:               250 ms
        rust-to-vir:             84 ms
        verify:                 157 ms
        erase:                    3 ms
    air-time:               347 ms
    smt-time:              2687 ms
        smt-init:                 0 ms
        smt-run:               2687 ms

[parno]

I notice that the problematic lemma, lemma_interp_of_entries_disjoint, uses two non-linear queries. Historically, such queries have been notoriously flaky, so I'm curious if that's playing a role here. One experiment would be to replace the assert_nonlinear_bys with an assert for their requires and an assume for their ensures. That would still force Z3 to prove the assert_nonlinear_by's precondition and the function's post-condition. If the time for that is largely immune to the presence/absence of slow_down_everything, that would point the blame at the usual Z3 issues with non-linear queries.

[utaal]

(As a reminder, we're now using the new Z3 arithmetic solver for nonlinear queries, which appears generally better at discharging nonlinear queries, and still has performance implications, but with different behavior from the old solver.)

[matthias-brun]

@parno It's definitely related to the nonlinear queries. I haven't tried the exact experiment you suggest but during verification, Verus points out that it's waiting for the nonlinear assertions.

Chris' fix for #306 may have had an impact on this. I just tested the two most recent Verus commits for verifying just the specific lemma. Before Chris' fix the smt times are 3900ms and 24400ms. After the fix I'm getting 200ms and 1800ms. Still a big difference but both times are a lot faster. Not sure what to make of that. Maybe just instability?

[utaal]

As this is likely a case of instability, I've filed it as one of the instability cases to investigate: #147