search

rajathkotyal / verify-rust-std

Verifying the Rust standard library
https://model-checking.github.io/verify-rust-std/
Other
0 stars 0 forks source link

[P1-Unsafe Int] unchecked_sub #2

Closed rajathkotyal closed 1 month ago

rajathkotyal commented 2 months ago

Official Repo Tracking Issue

Tasks :

  1. Set up the necessary environment.
  2. Write individual proofs for verifying the absence of arithmetic overflow/underflow and undefined behavior for all integer types: i8, i16, i32, i64, i128, u8, u16, u32, u64, u128.
  3. Add proofs into a dedicated file. a. For example, library/core/src/num/mod.rs --> This will contain all proofs for unchecked_add/del/sub, etc.
  4. Please make sure not to modify other people's code, since we will be co-working on the same files. Avoid code conflicts as much as possible. Pull code every time a merge is made.

IMP: comment with the branch name you will be working on, with its link.

Ref: https://github.com/rajathkotyal/verify-rust-std/blob/main/doc/src/challenges/0011-floats-ints.md

Yenyun035 commented 1 month ago

Merged in PR#96.