> Soundness and panic semantics. Kani interprets Hoare triples under partial correctness with panic safety: [omitted] means that if [omitted] holds and [omitted] terminates normally (without panicking), then [omitted] holds. Panics (from assert!, unwrap(), arithmetic overflow, or outof-bounds access) are translated into assertion violations and are therefore checked as part of the verification. A successful Kani run guarantees both the absence of panics and the postcondition, for all inputs satisfying the precondition, up to the following assumptions: harness coverage of reachable inputs, aliasing closure of Mod for unsafe code, user-guaranteed termination, sequential execution (no threads or async), no Stacked Borrows [28] / Tree Borrows [44] pointer-aliasing modeling (the primary class of UB in unsafe Rust), and FFI calls executing outside CBMC’s memory model unless stubbed (§4.6). The last two are the most significant in practice. Miri [30] checks aliasing violations dynamically, making it a natural complement.
tl;dr: you still need to run miri and hope for the best lol
> Panics (from assert!, unwrap(), arithmetic overflow, or out- of-bounds access) are translated into assertion violations and are therefore checked as part of the verification. A successful Kani run guarantees both the absence of panics and the postcondition, for all inputs satisfying the precondition, up to the following assumptions: harness coverage of reachable inputs, aliasing closure of Mod for unsafe code, user-guaranteed termination, sequential execution (no threads or async), no Stacked Borrows [28] / Tree Borrows [44] pointer-aliasing modeling (the primary class of UB in unsafe Rust), and FFI calls executing outside CBMC’s memory model unless stubbed (§4.6). The last two are the most significant in practice. Miri [30] checks aliasing violations dynamically, making it a natural complement.
Bloody frauds, you must still run Miri and hope for the best.
You have now created four accounts to make basically this post, but the point is unclear. All of the highly automated theorem provers have some limitations to what they can guarantee, some of which comically strict. You are not really explaining how this operating on MIR makes it so distinctly useless/"fraudulent".
Is this only limited to (bounds|overflow|DBZ) checks? I do not know a lot about model checkers, it seems pretty cool though! and definitely something that would be powerful in a test harness
You aren't testing your application code directly, but writing a test function. That test function can include any assertion you want in the end, which causes a panic, failing the verification. Similarly you want to add assumptions in the test function for pre-conditions, so parameter verification assertions in the application won't fail the verification.
14 comments
[ 3.3 ms ] story [ 46.1 ms ] threadReminds me a bit of hypothesis auto in its simplest applications: https://github.com/timothycrosley/hypothesis-auto/
tl;dr: you still need to run miri and hope for the best lol
bloody frauds
The answer is yes:
> Soundness and panic semantics.
> (...)
> Panics (from assert!, unwrap(), arithmetic overflow, or out- of-bounds access) are translated into assertion violations and are therefore checked as part of the verification. A successful Kani run guarantees both the absence of panics and the postcondition, for all inputs satisfying the precondition, up to the following assumptions: harness coverage of reachable inputs, aliasing closure of Mod for unsafe code, user-guaranteed termination, sequential execution (no threads or async), no Stacked Borrows [28] / Tree Borrows [44] pointer-aliasing modeling (the primary class of UB in unsafe Rust), and FFI calls executing outside CBMC’s memory model unless stubbed (§4.6). The last two are the most significant in practice. Miri [30] checks aliasing violations dynamically, making it a natural complement.
Bloody frauds, you must still run Miri and hope for the best.
Kani Rust Verifier – a bit-precise model-checker for Rust - https://news.ycombinator.com/item?id=30786511 - March 2022 (12 comments)