Clarify the analysis technique used by Kani #2195
Conversation
docs/src/getting-started.md
Outdated
| Kani is particularly useful for verifying unsafe code in Rust, where many of the Rust’s usual guarantees are no longer checked by the compiler. | ||
| Some example properties you can prove with Kani include memory safety properties (e.g., null pointer dereferences, use-after-free, etc.), the absence of certain runtime errors (i.e., index out of bounds, panics), and the absence of some types of unexpected behavior (e.g., arithmetic overflows). | ||
| Kani can also prove custom properties provided in the form of user-specified assertions. | ||
| Many of these properties are undecidable in the general case. |
There was a problem hiding this comment.
I feel this is a bit too heavy for the getting started section. I suggest we move it to the the comparison with other tools section or paraphrase it a bit, e.g.:
Kani may not be able to solve all properties, in which case it may not terminate or may run out of memory.
Otherwise, Kani will either prove the property, or find a trace that leads to the violation of the property (e.g. the failure of an assertion).
There was a problem hiding this comment.
+1 to moving this to a different section. I was also wondering if we should call out here that the proof is under some constraints and add a link to the limitations section.
There was a problem hiding this comment.
+1 to moving it.
This paragraph should focus on what Kani can do, as opposed to what it cannot do. All tools have their limitations and it's OK with me to explain it in other sections, but we should keep it brief in order to keep readers engaged.
There was a problem hiding this comment.
I have removed the mention of "undecidable," and generalised the link to the Limitations section so as not to link into just a subsection.
| Kani is particularly useful for verifying unsafe code in Rust, where many of the Rust’s usual guarantees are no longer checked by the compiler. | ||
| Some example properties you can prove with Kani include memory safety properties (e.g., null pointer dereferences, use-after-free, etc.), the absence of certain runtime errors (i.e., index out of bounds, panics), and the absence of some types of unexpected behavior (e.g., arithmetic overflows). | ||
| Kani can also prove custom properties provided in the form of user-specified assertions. | ||
| Many of these properties are undecidable in the general case. | ||
| As Kani uses model checking, Kani will either prove the property, disprove the | ||
| property (with a counterexample), or may run out of resources. |
There was a problem hiding this comment.
| property (with a counterexample), or may run out of resources. | |
| property (providing you with a trace showing what input led to the property violation), or may run out of resources. |
I wonder if "trace" is more familiar to the reader than "counterexample"?
There was a problem hiding this comment.
I don't mind counterexample, since we are talking about what not how. Trace is one way of representing a counterexample. We also offer the concrete playback in which case the counterexample will be represented as a unit test.
There was a problem hiding this comment.
I think I like counterexample but not as a technical word, just as a phrase i.e disprove the property (with the example that fails the proof) or may run out of resources. Too many technical words in a page causes reading fatigue imo.
docs/src/getting-started.md
Outdated
| @@ -1,9 +1,11 @@ | |||
| # Getting started | |||
|
|
|||
| Kani is an open-source verification tool that uses automated reasoning to analyze Rust programs. | |||
| Kani is an open-source verification tool that uses [model checking](./tool-comparison.md) analyze Rust programs. | |||
There was a problem hiding this comment.
| Kani is an open-source verification tool that uses [model checking](./tool-comparison.md) analyze Rust programs. | |
| Kani is an open-source verification tool that uses [model checking](./tool-comparison.md) to analyze Rust programs. |
We use model checking - make clear what its limitations are when talking about what we may be able to prove.
We use model checking - make clear what its limitations are when talking about what we may be able to prove.
Description of changes:
Clarification of what Kani is in our documentation.
Resolved issues:
n/a
Related RFC:
n/a
Call-outs:
n/a
Testing:
n/a
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.