Skip to content

Commit 367d8ff

Browse files
lang280lang280
authored
NonZero (rotate_left, rotate_right, max, min, clamp, count_ones, cmp) Proofs (#202)
Working on [#71](#71) (Safety of NonZero) We are looking for feedback on our proof for rotate_left & rotate_right. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 8a248d9 commit 367d8ff

File tree

1 file changed

+220
-0
lines changed

1 file changed

+220
-0
lines changed

‎library/core/src/num/nonzero.rs‎

Lines changed: 220 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2264,4 +2264,224 @@ mod verify {
22642264
nonzero_check!(u64, core::num::NonZeroU64, nonzero_check_new_unchecked_for_u64);
22652265
nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128);
22662266
nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize);
2267+
2268+
macro_rules! nonzero_check_cmp {
2269+
($nonzero_type:ty, $nonzero_check_cmp_for:ident) => {
2270+
#[kani::proof]
2271+
pub fn $nonzero_check_cmp_for() {
2272+
let x: $nonzero_type = kani::any();
2273+
let y: $nonzero_type = kani::any();
2274+
if x < y {
2275+
assert!(x.cmp(&y) == core::cmp::Ordering::Less);
2276+
} else if x > y {
2277+
assert!(x.cmp(&y) == core::cmp::Ordering::Greater);
2278+
} else {
2279+
assert!(x.cmp(&y) == core::cmp::Ordering::Equal);
2280+
}
2281+
}
2282+
};
2283+
}
2284+
2285+
// Use the macro to generate different versions of the function for multiple types
2286+
nonzero_check_cmp!(core::num::NonZeroI8, nonzero_check_cmp_for_i8);
2287+
nonzero_check_cmp!(core::num::NonZeroI16, nonzero_check_cmp_for_i16);
2288+
nonzero_check_cmp!(core::num::NonZeroI32, nonzero_check_cmp_for_i32);
2289+
nonzero_check_cmp!(core::num::NonZeroI64, nonzero_check_cmp_for_i64);
2290+
nonzero_check_cmp!(core::num::NonZeroI128, nonzero_check_cmp_for_i128);
2291+
nonzero_check_cmp!(core::num::NonZeroIsize, nonzero_check_cmp_for_isize);
2292+
nonzero_check_cmp!(core::num::NonZeroU8, nonzero_check_cmp_for_u8);
2293+
nonzero_check_cmp!(core::num::NonZeroU16, nonzero_check_cmp_for_u16);
2294+
nonzero_check_cmp!(core::num::NonZeroU32, nonzero_check_cmp_for_u32);
2295+
nonzero_check_cmp!(core::num::NonZeroU64, nonzero_check_cmp_for_u64);
2296+
nonzero_check_cmp!(core::num::NonZeroU128, nonzero_check_cmp_for_u128);
2297+
nonzero_check_cmp!(core::num::NonZeroUsize, nonzero_check_cmp_for_usize);
2298+
2299+
2300+
macro_rules! nonzero_check_max {
2301+
($nonzero_type:ty, $nonzero_check_max_for:ident) => {
2302+
#[kani::proof]
2303+
pub fn $nonzero_check_max_for() {
2304+
let x: $nonzero_type = kani::any();
2305+
let y: $nonzero_type = kani::any();
2306+
let result = x.max(y);
2307+
if x > y {
2308+
assert!(result == x);
2309+
} else {
2310+
assert!(result == y);
2311+
}
2312+
}
2313+
};
2314+
}
2315+
2316+
nonzero_check_max!(core::num::NonZeroI8, nonzero_check_max_for_i8);
2317+
nonzero_check_max!(core::num::NonZeroI16, nonzero_check_max_for_i16);
2318+
nonzero_check_max!(core::num::NonZeroI32, nonzero_check_max_for_i32);
2319+
nonzero_check_max!(core::num::NonZeroI64, nonzero_check_max_for_i64);
2320+
nonzero_check_max!(core::num::NonZeroI128, nonzero_check_max_for_i128);
2321+
nonzero_check_max!(core::num::NonZeroIsize, nonzero_check_max_for_isize);
2322+
nonzero_check_max!(core::num::NonZeroU8, nonzero_check_max_for_u8);
2323+
nonzero_check_max!(core::num::NonZeroU16, nonzero_check_max_for_u16);
2324+
nonzero_check_max!(core::num::NonZeroU32, nonzero_check_max_for_u32);
2325+
nonzero_check_max!(core::num::NonZeroU64, nonzero_check_max_for_u64);
2326+
nonzero_check_max!(core::num::NonZeroU128, nonzero_check_max_for_u128);
2327+
nonzero_check_max!(core::num::NonZeroUsize, nonzero_check_max_for_usize);
2328+
2329+
2330+
macro_rules! nonzero_check_min {
2331+
($nonzero_type:ty, $nonzero_check_min_for:ident) => {
2332+
#[kani::proof]
2333+
pub fn $nonzero_check_min_for() {
2334+
let x: $nonzero_type = kani::any();
2335+
let y: $nonzero_type = kani::any();
2336+
let result = x.min(y);
2337+
if x < y {
2338+
assert!(result == x);
2339+
} else {
2340+
assert!(result == y);
2341+
}
2342+
}
2343+
};
2344+
}
2345+
2346+
nonzero_check_min!(core::num::NonZeroI8, nonzero_check_min_for_i8);
2347+
nonzero_check_min!(core::num::NonZeroI16, nonzero_check_min_for_i16);
2348+
nonzero_check_min!(core::num::NonZeroI32, nonzero_check_min_for_i32);
2349+
nonzero_check_min!(core::num::NonZeroI64, nonzero_check_min_for_i64);
2350+
nonzero_check_min!(core::num::NonZeroI128, nonzero_check_min_for_i128);
2351+
nonzero_check_min!(core::num::NonZeroIsize, nonzero_check_min_for_isize);
2352+
nonzero_check_min!(core::num::NonZeroU8, nonzero_check_min_for_u8);
2353+
nonzero_check_min!(core::num::NonZeroU16, nonzero_check_min_for_u16);
2354+
nonzero_check_min!(core::num::NonZeroU32, nonzero_check_min_for_u32);
2355+
nonzero_check_min!(core::num::NonZeroU64, nonzero_check_min_for_u64);
2356+
nonzero_check_min!(core::num::NonZeroU128, nonzero_check_min_for_u128);
2357+
nonzero_check_min!(core::num::NonZeroUsize, nonzero_check_min_for_usize);
2358+
2359+
2360+
macro_rules! nonzero_check_clamp {
2361+
($nonzero_type:ty, $nonzero_check_clamp_for:ident) => {
2362+
#[kani::proof]
2363+
pub fn $nonzero_check_clamp_for() {
2364+
let x: $nonzero_type = kani::any();
2365+
let min: $nonzero_type = kani::any();
2366+
let max: $nonzero_type = kani::any();
2367+
// Ensure min <= max, so the function should no panic
2368+
kani::assume(min <= max);
2369+
// Use the clamp function and check the result
2370+
let result = x.clamp(min, max);
2371+
if x < min {
2372+
assert!(result == min);
2373+
} else if x > max {
2374+
assert!(result == max);
2375+
} else {
2376+
assert!(result == x);
2377+
}
2378+
}
2379+
};
2380+
}
2381+
2382+
// Use the macro to generate different versions of the function for multiple types
2383+
nonzero_check_clamp!(core::num::NonZeroI8, nonzero_check_clamp_for_i8);
2384+
nonzero_check_clamp!(core::num::NonZeroI16, nonzero_check_clamp_for_16);
2385+
nonzero_check_clamp!(core::num::NonZeroI32, nonzero_check_clamp_for_32);
2386+
nonzero_check_clamp!(core::num::NonZeroI64, nonzero_check_clamp_for_64);
2387+
nonzero_check_clamp!(core::num::NonZeroI128, nonzero_check_clamp_for_128);
2388+
nonzero_check_clamp!(core::num::NonZeroIsize, nonzero_check_clamp_for_isize);
2389+
nonzero_check_clamp!(core::num::NonZeroU8, nonzero_check_clamp_for_u8);
2390+
nonzero_check_clamp!(core::num::NonZeroU16, nonzero_check_clamp_for_u16);
2391+
nonzero_check_clamp!(core::num::NonZeroU32, nonzero_check_clamp_for_u32);
2392+
nonzero_check_clamp!(core::num::NonZeroU64, nonzero_check_clamp_for_u64);
2393+
nonzero_check_clamp!(core::num::NonZeroU128, nonzero_check_clamp_for_u128);
2394+
nonzero_check_clamp!(core::num::NonZeroUsize, nonzero_check_clamp_for_usize);
2395+
2396+
2397+
macro_rules! nonzero_check_clamp_panic {
2398+
($nonzero_type:ty, $nonzero_check_clamp_for:ident) => {
2399+
#[kani::proof]
2400+
#[kani::should_panic]
2401+
pub fn $nonzero_check_clamp_for() {
2402+
let x: $nonzero_type = kani::any();
2403+
let min: $nonzero_type = kani::any();
2404+
let max: $nonzero_type = kani::any();
2405+
// Ensure min > max, so the function should panic
2406+
kani::assume(min > max);
2407+
// Use the clamp function and check the result
2408+
let result = x.clamp(min, max);
2409+
if x < min {
2410+
assert!(result == min);
2411+
} else if x > max {
2412+
assert!(result == max);
2413+
} else {
2414+
assert!(result == x);
2415+
}
2416+
}
2417+
};
2418+
}
2419+
2420+
// Use the macro to generate different versions of the function for multiple types
2421+
nonzero_check_clamp_panic!(core::num::NonZeroI8, nonzero_check_clamp_panic_for_i8);
2422+
nonzero_check_clamp_panic!(core::num::NonZeroI16, nonzero_check_clamp_panic_for_16);
2423+
nonzero_check_clamp_panic!(core::num::NonZeroI32, nonzero_check_clamp_panic_for_32);
2424+
nonzero_check_clamp_panic!(core::num::NonZeroI64, nonzero_check_clamp_panic_for_64);
2425+
nonzero_check_clamp_panic!(core::num::NonZeroI128, nonzero_check_clamp_panic_for_128);
2426+
nonzero_check_clamp_panic!(core::num::NonZeroIsize, nonzero_check_clamp_panic_for_isize);
2427+
nonzero_check_clamp_panic!(core::num::NonZeroU8, nonzero_check_clamp_panic_for_u8);
2428+
nonzero_check_clamp_panic!(core::num::NonZeroU16, nonzero_check_clamp_panic_for_u16);
2429+
nonzero_check_clamp_panic!(core::num::NonZeroU32, nonzero_check_clamp_panic_for_u32);
2430+
nonzero_check_clamp_panic!(core::num::NonZeroU64, nonzero_check_clamp_panic_for_u64);
2431+
nonzero_check_clamp_panic!(core::num::NonZeroU128, nonzero_check_clamp_panic_for_u128);
2432+
nonzero_check_clamp_panic!(core::num::NonZeroUsize, nonzero_check_clamp_panic_for_usize);
2433+
2434+
2435+
macro_rules! nonzero_check_count_ones {
2436+
($nonzero_type:ty, $nonzero_check_count_ones_for:ident) => {
2437+
#[kani::proof]
2438+
pub fn $nonzero_check_count_ones_for() {
2439+
let x: $nonzero_type = kani::any();
2440+
let result = x.count_ones();
2441+
// Since x is non-zero, count_ones should never return 0
2442+
assert!(result.get() > 0);
2443+
}
2444+
};
2445+
}
2446+
2447+
// Use the macro to generate different versions of the function for multiple types
2448+
nonzero_check_count_ones!(core::num::NonZeroI8, nonzero_check_count_ones_for_i8);
2449+
nonzero_check_count_ones!(core::num::NonZeroI16, nonzero_check_count_ones_for_i16);
2450+
nonzero_check_count_ones!(core::num::NonZeroI32, nonzero_check_count_ones_for_i32);
2451+
nonzero_check_count_ones!(core::num::NonZeroI64, nonzero_check_count_ones_for_i64);
2452+
nonzero_check_count_ones!(core::num::NonZeroI128, nonzero_check_count_ones_for_i128);
2453+
nonzero_check_count_ones!(core::num::NonZeroIsize, nonzero_check_count_ones_for_isize);
2454+
nonzero_check_count_ones!(core::num::NonZeroU8, nonzero_check_count_ones_for_u8);
2455+
nonzero_check_count_ones!(core::num::NonZeroU16, nonzero_check_count_ones_for_u16);
2456+
nonzero_check_count_ones!(core::num::NonZeroU32, nonzero_check_count_ones_for_u32);
2457+
nonzero_check_count_ones!(core::num::NonZeroU64, nonzero_check_count_ones_for_u64);
2458+
nonzero_check_count_ones!(core::num::NonZeroU128, nonzero_check_count_ones_for_u128);
2459+
nonzero_check_count_ones!(core::num::NonZeroUsize, nonzero_check_count_ones_for_usize);
2460+
2461+
2462+
macro_rules! nonzero_check_rotate_left_and_right {
2463+
($nonzero_type:ty, $nonzero_check_rotate_for:ident) => {
2464+
#[kani::proof]
2465+
pub fn $nonzero_check_rotate_for() {
2466+
let x: $nonzero_type = kani::any();
2467+
let n: u32 = kani::any();
2468+
let result = x.rotate_left(n).rotate_right(n);
2469+
assert!(result == x);
2470+
}
2471+
};
2472+
}
2473+
2474+
// Use the macro to generate different versions of the function for multiple types
2475+
nonzero_check_rotate_left_and_right!(core::num::NonZeroI8, nonzero_check_rotate_for_i8);
2476+
nonzero_check_rotate_left_and_right!(core::num::NonZeroI16, nonzero_check_rotate_for_i16);
2477+
nonzero_check_rotate_left_and_right!(core::num::NonZeroI32, nonzero_check_rotate_for_i32);
2478+
nonzero_check_rotate_left_and_right!(core::num::NonZeroI64, nonzero_check_rotate_for_i64);
2479+
nonzero_check_rotate_left_and_right!(core::num::NonZeroI128, nonzero_check_rotate_for_i128);
2480+
nonzero_check_rotate_left_and_right!(core::num::NonZeroIsize, nonzero_check_rotate_for_isize);
2481+
nonzero_check_rotate_left_and_right!(core::num::NonZeroU8, nonzero_check_rotate_for_u8);
2482+
nonzero_check_rotate_left_and_right!(core::num::NonZeroU16, nonzero_check_rotate_for_u16);
2483+
nonzero_check_rotate_left_and_right!(core::num::NonZeroU32, nonzero_check_rotate_for_u32);
2484+
nonzero_check_rotate_left_and_right!(core::num::NonZeroU64, nonzero_check_rotate_for_u64);
2485+
nonzero_check_rotate_left_and_right!(core::num::NonZeroU128, nonzero_check_rotate_for_u128);
2486+
nonzero_check_rotate_left_and_right!(core::num::NonZeroUsize, nonzero_check_rotate_for_usize);
22672487
}

0 commit comments

Comments
 (0)