kani
kani copied to clipboard
model-checking
question: semantics of rust
Hi,
I have a question as to the intended rust semantics that Kani implements, and an improvement request to document the answer to this question in the README :)
- Do you basically do what rustc does?
- Do you do what ferrocene specifies?
- Something else entirely?
Thanks!
That's a great question, and I agree that we need to improve our documentation. We have been mostly using the following as the source of the Rust semantics sorted by the order of priority:
- The Rust reference book
- The Rust Standard Library documentation
- The Rust RFC book / tracking issues for unstable features
- The decisions made by the unsafe code guidelines group.
- Rustc / MIRI implementations / Zulip discussions
Additionally, we encode memory following CBMC memory model. Every allocation and stack variables are assigned a unique identifier, which is part of the pointer address itself. CBMC track variable liveness and allocation statuses using ghost code.
Excellent, thank you for the detailed answer!
So just to confirm, you're not following the ferrocene lrm in any way? I suppose if they want to have Kani support, then they would also need to fork kani, just like they forked rustc?
Excellent, thank you for the detailed answer!
So just to confirm, you're not following the ferrocene lrm in any way? I suppose if they want to have Kani support, then they would also need to fork kani, just like they forked rustc?
It's not clear to me how they are implementing their specification. They could potentially fork Kani, or extend Kani (it depends how much their rustc implementation has diverged). This is something we would have to discuss with them if there's ever interest in verifying their specification.
(it depends how much their rustc implementation has diverged)
Supposedly it's just unmodified upstream rustc:
https://ferrous-systems.com/blog/qualifying-rust-without-forking/
So it should be fairly straightforward to extend Kani to support their specification