[P1-Unsafe Int] unchecked_neg

[parkerqi]

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.
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]

@parkerqi Could you take a look at the proofs written by the others? Mainly two points:

1. Add a function contract (requires) to unchecked_neg method.
2. Write harnesses with proof_for_contract(<type>::unchecked_neg) attribute. You don't need kani::assume and assert if using this one.

[Yenyun035]

PR#102

[Yenyun035]

Merged in PR#102