Add missing safety documentation and assertions for testing and fuzzing

[ia0]

No description provided.

[thalesfragoso]

Aliasing debug_assert! as safety_assert! seems quite misleading, and I also wouldn't consider it enough to change the function to safe, since it only happens in a specific profile.

I know that the functions are internal, but I think having an unsafe function marked as safe is error prone to future contributions.

[ia0]

Aliasing debug_assert! as safety_assert! seems quite misleading, and I also wouldn't consider it enough to change the function to safe, since it only happens in a specific profile.

You're probably assuming more than what is meant. The usage of safety_assert! is just invariant documentation (for safety comments) in the form of code. It is not supposed to change the behavior of the code. The fact that debug builds will execute something is just for dynamic testing purposes (making sure the assertion never fails). The function behaves exactly the same (since the assert will never fail and is thus a no-op). That's exactly the same usage as debug assertions. The name is just to easily refer to it from a safety comment.

I know that the functions are internal, but I think having an unsafe function marked as safe is error prone to future contributions.

I agree that it's not a great style but I'm also not convinced by duplicating the proof work for both correctness and soundness, since correctness implies soundness and this crate aims for correctness, not just soundness. That might change if I use a tool which enforces semantically unsafe private functions to be marked unsafe (VeriFast is such a tool). But that would most probably only happen in v3. I have enough confidence with fuzzing and absence of bugs in 8 years that v2 is correct.

I'm not expecting contributions. I address feature requests (and any other issues) within a week and release within the next week. If someone wants to contribute, I would expect them to read everything that depends on the part they are modifying. Adding a new encoding constant doesn't need to understand much since nothing depends on it. But modifying such deep part of the library, needs to understand the complete library and its correctness proof.

What is triggering your question? Are you interested to contribute? If yes, I would highly suggest looking at v3 (which I temporarily removed but should add back in the lib/v3 folder when I get time).