[P1-Unsafe Int] unchecked_add

[rajathkotyal]

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]

Working branch: c-0011-core-nums-yenyunw-unsafe-ints

Verification code location: module verify in library/core/src/num/mod.rs

[Yenyun035]

TODO:

• [x] Relocate the proof module to library/core/src/num/mod.rs (or int_macros.rs?)
• [x] Rewrite unchecked_add proofs
  • [x] i8
  • [x] i16
  • [x] i32
  • [x] i64
  • [x] i128
  • [x] u8
  • [x] u16
  • [x] u32
  • [x] u64
  • [x] u128
• [x] Run proofs and get results

[rajathkotyal]

Nicely done! Tag me in the issues as well if you have any doubts / important information, its easier to keep track.

[Yenyun035]

PR#91 merged