Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Contracts and Harnesses for unchecked_neg #102

Merged
merged 32 commits into from
Oct 8, 2024
Merged

Contracts and Harnesses for unchecked_neg #102

merged 32 commits into from
Oct 8, 2024

Conversation

Yenyun035
Copy link

@Yenyun035 Yenyun035 commented Oct 4, 2024 •
edited
Loading

Resolves #59

Changes

  • Added contracts for unchecked_neg (located in library/core/src/num/int_macros.rs)
  • Added a harness for unchecked_neg of each signed integer type
    • i8, i16, i32, i64, i128, isize --- 6 harnesses in total.
  • Fixed comments.

Revalidation

  1. Per the discussion in Challenge 11: Safety of Methods for Numeric Primitive Types #59, we have to build and run Kani from feature/verify-rust-std branch.
  2. To revalidate the verification results, run the following command. <harness_to_run> can be either num::verify to run all harnesses or num::verify::<harness_name> (e.g. check_unchecked_neg_i8) to run a specific harness.
kani verify-std  "path/to/library" \
    --harness <harness_to_run> \
    -Z unstable-options \
    -Z function-contracts \
    -Z mem-predicates

All default harnesses should pass.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

yew005 and others added 28 commits September 10, 2024 17:11
Add Kani proofs of unchecked_add for all integer types
1ae4c6d
Format proof files & Add verification function templates
b553678
Experiment with two verification approaches in mod.rs of core::num
daaaf7e
@Yenyun035
Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsa…
7bd0e3c 
…fe-ints
Add contracts to unchecked_add && Add i8::unchecked_add proof
1c9dbde
Format core::num mod.rs
894231f
Add comment for unchecked_add proofs
2bc4faf
Add harnesses for i16,i32,i64,i128 unchecked_add
d9d4b5f
Add harnesses for u8,u16,u32,u64,u128 unchecked_add
07c8b4a
Cleanup misplaced proofs
1fd4c6a
Clean up comment
b360311
Format comment
8cbca87
Remove before contracts. Fix import in
0eef858
Fix comment
4858a53
@Yenyun035
Merge branch 'main' into c-0011-core-nums-yenyunw-unsafe-ints
483bdf5
@Yenyun035
Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsa…
ce35002 
…fe-ints
Remove ensures contracts && Undo formatting on existing code
d99844d
Add {isize, usize}::unchecked_add harnesses
fbcf49e
@Yenyun035
Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsa…
457a2b5 
…fe-ints
Add harness generation macros for unchecked methods && Update uncheck…
54a03ef 
…ed_add harnesses
Remove unused import safety::ensures
8ee5682
@rajathkotyal
unchecked_mul and unchecked_shr proofs (#7)
02d706a 
* Added harnesses for unchecked multiplication (`unchecked_mul`) and shift right (`unchecked_shr`)
* Added a macro and input limits for multiplication proofs
* Reduced duplicity in code by using macros to generate proof harnesses
Add comments. Fix spacing
dce9e83
@rajathkotyal
Revert "Add comments. Fix spacing"
3880fc7 
This reverts commit dce9e83.
@rajathkotyal
Revert "unchecked_mul and unchecked_shr proofs (#7)"
781cb87 
This reverts commit 02d706a.
@Yenyun035
Merge branch 'main' into c-0011-core-nums-yenyunw-unsafe-ints
715e940
Add unchecked_neg contracts & harnesses
1f0f583
@Yenyun035
Merge branch 'main' of github.com:rajathkotyal/verify-rust-std into c…
a45a676 
…-0011-core-nums-yenyunw-unchecked-neg
@Yenyun035 Yenyun035 requested a review from a team as a code owner October 4, 2024 22:05
@Yenyun035 Yenyun035 mentioned this pull request Oct 4, 2024
Closed
zhassan-aws
zhassan-aws reviewed Oct 7, 2024
View reviewed changes
library/core/src/num/int_macros.rs Outdated Show resolved Hide resolved
library/core/src/num/mod.rs Show resolved Hide resolved
@Yenyun035
Copy link
Author

@zhassan-aws Thank you for your reviews! I have fixed the precondition for unchecked_neg and fixed some comments.

@Yenyun035
Copy link
Author

@feliperodri @celinval @carolynzech May I request the second approval to merge this PR? Thank you very much :)

celinval
celinval approved these changes Oct 8, 2024
View reviewed changes
Copy link

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@Yenyun035
Copy link
Author

@celinval @zhassan-aws Thank you! This PR can get merged now :)

@zhassan-aws zhassan-aws merged commit 32e0cf9 into model-checking:main Oct 8, 2024
7 of 8 checks passed
@Yenyun035 Yenyun035 deleted the c-0011-core-nums-yenyunw-unchecked-neg branch November 27, 2024 08:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@zhassan-aws zhassan-aws zhassan-aws approved these changes

@celinval celinval celinval approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Challenge 11: Safety of Methods for Numeric Primitive Types
4 participants
@Yenyun035 @celinval @zhassan-aws @rajathkotyal