Safety audit and comments#22
Conversation
|
r? @dtolnay |
|
After doing this I realized you are performing line-by-line syncs, presumably in an automated fashion. Is there a way we can have that and still have safety comments? |
dtolnay
left a comment
There was a problem hiding this comment.
Thanks!
This is focused on making the Rust code more auditable, and I am not interested in accepting it for that purpose. The best way to audit this library would be to audit the original C++ implementation, and then audit the port by comparing the two implementations side-by-side. The former doesn't benefit from Rust comments and the latter is hindered by unnecessary divergence between the implementations, including comments and assertions.
Where there are undocumented nontrivial mathematical invariants I would recommend sending comments upstream and they will get mirrored here.
|
Rust unsafe is not the same as C++ unsafe. Rust has unsafe rules that do not matter for C++. As someone who has audited a lot of unsafe code, a large chunk of Rust UB cases are ones where the author assumed Rust worked like C++ and got it wrong (e.g. around provenance or uninitialized memory). I think there is almost no chance that a C++ library will accept safety comments to the level that is useful for Rust. C++ just doesn't have that culture of safety comments. I still asked, though vitaut/zmij#130 That would still be quite suboptimal: those comments would be in terms of C++ operations, not the Rust operations. I don't really think it would achieve the goals here. How are you performing the mirroring? I'm happy to tweak these to work with the mirroring process better. Some ideas would be maintaining a rebasable patch on top of the C++ code that adds comments, or maybe having a pattern list of unsafe blocks in a separate file.
Well, really, documenting an audit and making it easy for people to verify, especially as the code changes in the future. I think that's useful for users of this crate. |
This is a lot of unsafe code relying on nontrivial mathematical invariants. I tried to add safety comments so we can more easily prove the safety of this code.
I used Gemini a bit to do some of the more tedious tracking.