address last bits of feedback

Author: AlexanderPortland

rfc/src/rfcs/0014-harness-partition.md

@@ -10,6 +10,7 @@
 ## Summary
 
 It can often be useful to subdivide an expensive proof harness so that different parts of the input space are verified separately.
+This is also known as *proof by cases* or a *case split*.
 Adding the built-in ability to partition a proof harness into different pieces (that each make differing assumptions about their inputs) could reduce the cost of expensive proofs, while allowing Kani to automatically check that the partitions cover the entire input space and, thus, will be equivalent to a single-harness proof.
 
 ## User Impact
@@ -34,7 +35,7 @@ pub fn proof_harness() {
 ```
 
 Since there are two tricky to analyze function calls, but only one will ever be called on a given input, you might want to verify all values of `input` where `input > 0` that will take the first branch separately from those that will take the second.
-This way, each solve will only have to reason about two of the three complex function calls, and you could use Kani's parallel proof runner to run both proofs at once.
+This way, each verification run will only have to reason about two of the three complex function calls, and you could use Kani's parallel proof runner to run both proofs at once.
 
 The best way to currently do this is by manually partitioning out these paths into two proof harnesses.
 
@@ -56,7 +57,7 @@ One could also write preconditions for `very_complex_fn_{1_2}` that restrict `in
 
 However, either of these strategies:
 - **can affect soundness**--there's no guarantee that your partitions will fully span the space of possible inputs.
-The only way to determine that a set of proofs like the one above are incorrect (as it forgets to verify the value of 0 for `input`) is by manual inspection.
+The only way to determine that a set of proofs like the one above are incomplete (as it forgets to verify the value of 0 for `input`) is by manual inspection.
 This gets infeasible for proofs with complex partition rules like those found in the [proofs for the standard library's unchecked multiplication](https://github.com/model-checking/verify-rust-std/blob/1c4ea17a99b9202f96608473083998b116bb6508/library/core/src/num/mod.rs#L1818-L1836).
 - **increases user burden**--instead of having to write and maintain a single proof, the user now has to handle a proof for each partition.
 
@@ -72,7 +73,7 @@ For example, the above would become
 ```rust
 #[kani::proof]
 pub fn partitioned_proof() {
-    kani::partition::<i32>([|a| *a > 0, |a| *a < 0], |input: i32| target_fn(input));
+    kani::partition::<i32, _, _>([|a| *a > 0, |a| *a < 0], |input: i32| assert!(target_fn(input) > 0));
 }
 ```
 
@@ -124,15 +125,15 @@ pub fn partition<T: Arbitrary, R, const N: usize>(
 ```
 
 This signature makes a few key design decisions:
-- *It takes in an array of `conditions` with the specific length `const N`*, ensuring the number of harnesses we have to generate is knowable at compile time when we're doing partition generation.
+- *It takes in an array of `conditions` with the specific length `const N`*, ensuring the number of harnesses we have to generate is known at compile time when we're doing partition generation.
 - *Partition conditions & the partition closure are represented by function pointers*.
 This allows the user to provide closures of the same signature, but only if those closures do not capture any state.
 Allowing conditions closures to capture runtime state like local variables would be unwise as partitions are conceptually static divisions of a proof which should not depend on runtime values.
 - *The function returns the same type `R` as the underlying partition closure*, with the thought being that value could then be used in later computation without affecting the mechanics of a partition.
 - *The partition variable is bound by `T: Arbitrary`*.
 This would allow us to construct a new non-deterministic value with `kani::any()` that can then be passed to the partition closure.
 
-When the `kani-compiler` encounters a call to this function, it will transparently replace the entire `#[kani::proof()]` that called it with a set of new generated functions that, as a whole, will represent the partitioned proof. This new partitioned proof would contain:
+When the `kani-compiler` encounters a call to this function, it will transparently replace the entire `#[kani::proof]` that called it with a set of new generated functions that, as a whole, will represent the partitioned proof. This new partitioned proof would contain:
 
 1. one new proof harness for each partition
 
@@ -145,7 +146,7 @@ pub fn partitioned_proof_partition_1() {
     /* OTHER CODE BEFORE THE CALL TO `kani::partition` IF THERE WAS ANY */
     let partition_variable = kani::any::<i32>();
     kani::assume((|a: &i32| *a > 0)(&partition_variable));
-    (|input: i32| target_fn(input))(partition_variable);
+    (|input: i32| assert!(target_fn(input) > 0))(partition_variable);
 }
 ```
 
@@ -180,13 +181,20 @@ pub fn strange_partitioned_proof() {
 ```
 
 The behavior of a partition in this case seems ill-defined, so Kani will detect cases where the partition conditions are not constant closures or function items and emit a compile error.
+This would likely require new analysis from Kani to properly detect these cases.
 
 ## Rationale and alternatives
 
-### 1. Allowing overlapping partition conditions
+### 1. `kani::partition` as an attribute
+We had initially considered implementing the partition as an attribute placed on a proof harness, similar to `kani::proof`.
+However, we decided it would be best implemented as a function because a partition conceptually represents a split on variables in the proof, rather than something inherent to the proof itself.
+Similarly, we wanted to maintain the convention that proof harnesses do not take in any inputs, and all attribute solutions would have to break that.
+
+### 2. Allowing overlapping partition conditions
 As a corollary to checking that partitions span the space of all possible inputs, I had initially considered giving a warning if partitions are overlapping as this could indicate ill-defined bounds.
 
-However, this kind of overlap would not affect the correctness of the partition, as every possible value of the partition variable would still be checked, just potentially more than once. Admittedly, it's fairly difficult to come up with a realistic use case in which an overlap is helpful for users, so whether this should be allowed is up for debate.
+However, this kind of overlap would not affect the correctness of the partition, as every possible value of the partition variable would still be checked, just potentially more than once.
+Admittedly, it's fairly difficult to come up with a realistic use case in which an overlap is helpful for users, so whether this should be allowed is up for debate.
 
 ## Open questions
 
@@ -199,6 +207,7 @@ Potentially through a separate function `partition_bounded` which would be gener
 Users may only want to test a subset of the input space (e.g., only testing multiplication for certain integer ranges), but the current design mandates that they cover the whole input space.
 We could potentially introduce a separate API, e.g. `unsafe_partition`, that allows this, or some other mechanism to skip the coverage check.
 6. Should overlapping partition conditions be allowed?
-7. Can we tell the user which section(s) of the input space they're missing?
+7. (Similar to #3) How can a coverage check failure be best presented to users?
+Perhaps by running the coverage harness with concrete playback to generate a test case that doesn't fall into the partitions?
 
 [^unstable_feature]: This unique ident should be used to enable features proposed in the RFC using `-Z <ident>` until the feature has been stabilized.