[Aurel300]

Yes, we could improve the wording -- suggestions and users are welcome! The tool is indeed much more general purpose than integer overflows: it is a based on a deductive verifier which uses symbolic execution to figure out which nodes in the CFG are reachable and under what conditions. panic!, unreachable!, failed assert!s, etc are all checked. If one can be reached, the error to show to the user is reconstructed from the compiler's span information.

[hn92726819]

If I'm reading your comment correctly, then this is so much cooler than I thought :D. Closest thing to this would be https://docs.rs/no-panic/latest/no_panic/ I believe, and the error message leaves much to be desired.

I will definitely be trying this out, but one last question: std can panic when doing tons of things (slice indexing, str.split_at, etc). Can this be used to make never-panicing programs?

[Aurel300]

The short answer is: it could be used for that. But there's a couple of things to say:

- Prusti is doing _modular_ verification: every method is verified in isolation, and all calls in that method's code only use the contracts declared on the call targets. This is good for scalability and caching and it means that a method's signature + contract is the entire API (you don't depend on its internals).

- Methods without a contract are assumed to have the precondition `true` and postcondition `true` (in other words, such a method can always be called and makes no guarantees at all about what it did to its mutable arguments or result). For methods declared within the current project, this is fine: if they could panic, Prusti would identify this when verifying them and the user would have to declare a precondition. For external methods (whose implementation is not verified), this is potentially unsound.

- However, we are in the process of creating a library of specifications for stdlib methods. We use a large-scale analysis framework (rust-corpus/qrates) to evaluate which methods are used most often. We try to specify such methods first to cover real-world Rust code usages.

Making the default precondition for external functions "false" (unless specified otherwise) would be sound but would be quite restrictive. One goal of Prusti is also incremental verification: you should be able to start using Prusti for basic checks then gradually introduce more specifications to get stronger and stronger guarantees about the program's behaviour.

[nextaccountic]

> - However, we are in the process of creating a library of specifications for stdlib methods. We use a large-scale analysis framework (rust-corpus/qrates) to evaluate which methods are used most often. We try to specify such methods first to cover real-world Rust code usages.

I asked somewhere else about the difference of prusti and mirai but, could mirai also make use of this specification?

I see that prusti_contracts and the contracts crate have a different syntax, but many contracts written for one could be translated for other, right? (IOW I don't know how much their semantics differ)

[epilys]

Thanks for your interesting work! I wanted to ask, how are FFI boundaries handled? Are they ignored or is it an error to call FFI functions?

[Aurel300]

Currently they are not handled. But (you guessed it) we also have a project working on this: attaching trusted specifications to external methods.

In the long term we might investigate a full integration with external verifiers, e.g. to check that the specifications declared on external methods in Rust is justified by their actual implementation, say in C. This is tricky because the specification language/level of abstraction might differ. It might be necessary to prove program refinement, for example.

[epilys]

Sounds really exciting! Mir interpreter has the same limitation. Have you examined incorporating mir in your analysis?

[Aurel300]

Our verification is based on symbolic execution, miri is an interpreter (concrete execution). So (at least in theory), our approach is more general. We have considered miri in relation to counterexamples: when Prusti emits an assertion failure and gives an example set of values that would lead to such a failure, we could use miri to make sure the counterexample is not spurious (which could happen with certain loop invariants IIRC). However, we have not implemented anything concrete yet.