RFC: Partitioned proofs

[AlexanderPortland]

This discusses a prototype implementation of the feature suggested in #3006 that would allow users to soundly partition proofs into harnesses that could be verified separately and in parallel.

Rendered

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[carolynzech]

Thanks! First round of comments. Remember to update SUMMARY.md!

[tautschnig]

The various comments need to be driven to a conclusion, but I'm certainly supportive of the overall idea.

[AlexanderPortland]

Carolyn and I just had a talk about the syntax thoughts discussed above and echoed by Sammy here, and we started to converge on an idea that seems compelling. (Just dumping our thoughts here now until I have time to edit the RFC at a later date)

The initial syntax of kani::partition([i > 0, i < 0], || target_fn(input)) has some great benefits, mainly a) tying the partition conditions directly to the part of the proof being partitioned (rather than associating them with the whole harness) and b) maintaining the very logical idiom that harnesses don't take any arguments.

However, this syntax also brings up some questions, such as how a condition like i > 0 knows that it's operating over the input variable without relying solely on them sharing an ident, and how to ensure that input is filtered to be within the bounds of the partition after it has already been captured by the || target_fn(input) closure.

To fix this, we discussed a new API where partition would be a function Kani users can call with the following signature. The compiler would then detect this call within a proof, and generate the multiple partition harnesses, with each kani::assume-ing for a different one of the partition conditions.

pub fn partition<T: Arbitrary, R, const N: usize>(
    variable: T,
    conditions: [fn(&T) -> bool; N],
    and_run: fn(T) -> R,
) -> R {
    // This inner code will likely be a compiler intrinsic, 
    // but is just included to get a sense of the logical shape for now
    let partition_num = /* DEPENDS ON PARTITION */;
    kani::assume(conditions[partition_num](&variable));
    and_run(variable)
}

Which could be called along the lines of

#[kani::proof]
pub fn partitioned_harness2() {
    let input = kani::any();
    let r = kani::partition(input, [|a| *a > 10, ...], |input| target_fn(input));
}

Some key notes:

• for now, both the conditions and and_run variables are function pointers, which forces them to not capture any variables. Allowing capturing of non-deterministic values (e.g. those generated with kani::any()) feels like it could lead to correctness issues, but this may be an overapproximation of a fix.
• for now, the T: Arbitrary bound ensures partitioning can only be done on types that can be generated from kani::any()--that seems like the most clear set of use cases. However, it may eventually be useful to relax that restriction in some cases where a non-Arbitrary value is generated from an Arbitrary one, and i makes more sense for the partition to be defined on the latter.
• we'd likely want to prevent multiple calls to kani::partition within the same proof, as this could lead to exponential growth in the number of generated harnesses

(Will add these to the RFC's open questions when I have time)

[AlexanderPortland]

When working on a second draft of this RFC, I encountered a potential issue with the above syntax. Consider the following proof harness:

#[kani::proof]
pub fn strange_partitioned_harness() {
    let input: i32 = kani::any();

    let f: fn(&i32) -> bool = if input > 10 {
        |a: &i32| *a < 0
    } else {
        |a: &i32| *a < -2
    };

    kani::partition(input, [f, |a| *a >= 0], |i| target_fn(i));
}

Since one of the partition conditions depends on the non-deterministic partition variable, it seems almost non-sensical, as partition conditions should just be pre-defined filters to split that variable, rather than a function determined by runtime values.

To fix this, I tried forcing the conditions array to be compile-time evaluable by making it a const generic (with the signature below), but then the compiler complained saying "the type of const parameters must not depend on other generic parameters".

pub fn partition<T: kani::Arbitrary, R, const N: usize, const C: [fn(&T) -> bool; N]>(
    variable: T,
    conditions: C,
    and_run: fn(T) -> R,
) -> R

Is there a better way to ensure that the value of the function pointers we get can't be impacted by non-det values?

[AlexanderPortland]

Second draft of this RFC! Note that in discussion w/ @carolynzech and @camelid, the issue raised in my comment above should be fixed in this newly proposed API if we also check the validity of partition conditions.

[carolynzech]

Thanks! This is looking great.

[zhassan-aws]

Nice, thanks! Some minor comments.