Skip to content

NonZero (max & min) Proof #199

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

Closed
lang280 wants to merge 5 commits into from
Closed

NonZero (max & min) Proof #199

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
1812ba9
max_min
lang280 Dec 1, 2024
c9e1c21
Merge branch 'model-checking:main' into Nonezero_max_min
lang280 Dec 3, 2024
2af75f9
avoid name reused in min and max
lang280 Dec 3, 2024
afc4d5f
avoid use of unsafe code block by generate nonezero from any() directly
lang280 Dec 4, 2024
1cc63fc
Merge branch 'main' into Nonezero_max_min
Dec 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
66 changes: 66 additions & 0 deletions library/core/src/num/nonzero.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2265,3 +2265,69 @@ mod verify {
nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128);
nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize);
}

#[cfg(kani)]
mod macro_nonzero_check_max {

@carolynzech carolynzech Dec 5, 2024

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

Nice! Last thing -- instead of having a module for each function, can you move all of these harnesses inside of mod verify? We're trying to keep a consistent format for these proofs across challenges, and that's how we've been doing it so far.

@lang280 lang280 Dec 10, 2024

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

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

I have done this in NonZero (rotate_left & rotate_right) Proof #202

@tautschnig tautschnig Dec 10, 2024

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Sure, but could you please also do it here?

use super::*;
macro_rules! nonzero_check_max {
($nonzero_type:ty, $nonzero_check_max_for:ident) => {
#[kani::proof]
pub fn $nonzero_check_max_for() {
let x: $nonzero_type = kani::any();
let y: $nonzero_type = kani::any();
let result = x.max(y);
if x > y {
assert!(result == x);
} else {
assert!(result == y);
}
}
};
}

nonzero_check_max!(core::num::NonZeroI8, nonzero_check_max_for_i8);
nonzero_check_max!(core::num::NonZeroI16, nonzero_check_max_for_i16);
nonzero_check_max!(core::num::NonZeroI32, nonzero_check_max_for_i32);
nonzero_check_max!(core::num::NonZeroI64, nonzero_check_max_for_i64);
nonzero_check_max!(core::num::NonZeroI128, nonzero_check_max_for_i128);
nonzero_check_max!(core::num::NonZeroIsize, nonzero_check_max_for_isize);
nonzero_check_max!(core::num::NonZeroU8, nonzero_check_max_for_u8);
nonzero_check_max!(core::num::NonZeroU16, nonzero_check_max_for_u16);
nonzero_check_max!(core::num::NonZeroU32, nonzero_check_max_for_u32);
nonzero_check_max!(core::num::NonZeroU64, nonzero_check_max_for_u64);
nonzero_check_max!(core::num::NonZeroU128, nonzero_check_max_for_u128);
nonzero_check_max!(core::num::NonZeroUsize, nonzero_check_max_for_usize);
}

#[cfg(kani)]
mod macro_nonzero_check_min {
use super::*;
macro_rules! nonzero_check_min {
($nonzero_type:ty, $nonzero_check_min_for:ident) => {
#[kani::proof]
pub fn $nonzero_check_min_for() {
let x: $nonzero_type = kani::any();
let y: $nonzero_type = kani::any();
let result = x.min(y);
if x < y {
assert!(result == x);
} else {
assert!(result == y);
}
}
};
}

nonzero_check_min!(core::num::NonZeroI8, nonzero_check_min_for_i8);
nonzero_check_min!(core::num::NonZeroI16, nonzero_check_min_for_i16);
nonzero_check_min!(core::num::NonZeroI32, nonzero_check_min_for_i32);
nonzero_check_min!(core::num::NonZeroI64, nonzero_check_min_for_i64);
nonzero_check_min!(core::num::NonZeroI128, nonzero_check_min_for_i128);
nonzero_check_min!(core::num::NonZeroIsize, nonzero_check_min_for_isize);
nonzero_check_min!(core::num::NonZeroU8, nonzero_check_min_for_u8);
nonzero_check_min!(core::num::NonZeroU16, nonzero_check_min_for_u16);
nonzero_check_min!(core::num::NonZeroU32, nonzero_check_min_for_u32);
nonzero_check_min!(core::num::NonZeroU64, nonzero_check_min_for_u64);
nonzero_check_min!(core::num::NonZeroU128, nonzero_check_min_for_u128);
nonzero_check_min!(core::num::NonZeroUsize, nonzero_check_min_for_usize);
}