Verification time for conjunctions in `(prusti_)assert`

[Patrick-6]

This program contains 6 different ways of asserting a long conjunction, either with assert or prusti_assert, and then either with the short-circuiting and &&, the non-short-circuiting and &, or by separating the assertions into separate statements:

#![allow(unused)]
use prusti_contracts::*;

#[requires(x > 10)]
fn _test_prusti_assert_speed(x: i32) {
    let b = [f(x), f(2 * x), f(x - 1), f(x / 2 + 20)];

    prusti_assert!(b[0] && b[1] && b[2] && b[3] && b[0] && b[1] && b[2] && b[3] && b[0] && b[1] && b[2] && b[3] && b[0] && b[1] && b[2] && b[3]);

    // prusti_assert!(b[0] & b[1] & b[2] & b[3] & b[0] & b[1] & b[2] & b[3] & b[0] & b[1] & b[2] & b[3] & b[0] & b[1] & b[2] & b[3]);

    // prusti_assert!(b[0]); prusti_assert!(b[1]); prusti_assert!(b[2]); prusti_assert!(b[3]);
    // prusti_assert!(b[0]); prusti_assert!(b[1]); prusti_assert!(b[2]); prusti_assert!(b[3]);
    // prusti_assert!(b[0]); prusti_assert!(b[1]); prusti_assert!(b[2]); prusti_assert!(b[3]);
    // prusti_assert!(b[0]); prusti_assert!(b[1]); prusti_assert!(b[2]); prusti_assert!(b[3]);

    // assert!(b[0] && b[1] && b[2] && b[3] && b[0] && b[1] && b[2] && b[3] && b[0] && b[1] && b[2] && b[3] && b[0] && b[1] && b[2] && b[3]);
    
    // assert!(b[0] & b[1] & b[2] & b[3] & b[0] & b[1] & b[2] & b[3] & b[0] & b[1] & b[2] & b[3] & b[0] & b[1] & b[2] & b[3]);

    // assert!(b[0]); assert!(b[1]); assert!(b[2]); assert!(b[3]);
    // assert!(b[0]); assert!(b[1]); assert!(b[2]); assert!(b[3]);
    // assert!(b[0]); assert!(b[1]); assert!(b[2]); assert!(b[3]);
    // assert!(b[0]); assert!(b[1]); assert!(b[2]); assert!(b[3]);
}

#[ensures(x >= 10 ==> result)]
fn f(x: i32) -> bool {
    true
}

Depending on which of them is uncommented, the crate has different verification performance, measured using cargo prusti --timings, and ignoring the time taken to compile prusti-contracts:

Type	Subtype	Times for verification [seconds]	Mean time
prusti_assert	&&	49.07 49.13 48.58 48.68	48.87
prusti_assert	&	5.52 5.59 5.52 5.5	5.53
prusti_assert	separate	6.45 6.37 6.26 6.32	6.35
assert	&&	9.61 9.47 9.43 9.45	9.49
assert	&	11.68 11.69 11.73 11.79	11.72
assert	separate	12.07 12.02 12.16 11.75	12.00

(Tested with Prusti version: 0.2.2, commit 9934ff4 2023-04-05 13:46:10 UTC, built on 2023-04-05 13:56:02 UTC rustc 1.70.0-nightly (e3dfeeaa4 2023-03-07), on WSL1, Ubuntu 22.04, on a Ryzen 9 5900X)

Since the expression in a prusti_assert statement has to be pure, it might be possible for Prusti to automatically turn all the && in such an expression into & for better verification performance.

Also, if Prusti could detect that the condition in an assert statement is pure, maybe it could be turned into a prusti_assert.