@@ -2435,7 +2435,7 @@ mod verify {
24352435 }
24362436 } ;
24372437 }
2438-
2438+
24392439 // Generate harnesses for multiple types
24402440 nonzero_check_from_mut_unchecked ! ( i8 , core:: num:: NonZeroI8 , nonzero_check_from_mut_unchecked_i8) ;
24412441 nonzero_check_from_mut_unchecked ! ( i16 , core:: num:: NonZeroI16 , nonzero_check_from_mut_unchecked_i16) ;
@@ -2449,22 +2449,6 @@ mod verify {
24492449 nonzero_check_from_mut_unchecked ! ( u64 , core:: num:: NonZeroU64 , nonzero_check_from_mut_unchecked_u64) ;
24502450 nonzero_check_from_mut_unchecked ! ( u128 , core:: num:: NonZeroU128 , nonzero_check_from_mut_unchecked_u128) ;
24512451 nonzero_check_from_mut_unchecked ! ( usize , core:: num:: NonZeroUsize , nonzero_check_from_mut_unchecked_usize) ;
2452-
2453-
2454-
2455- macro_rules! check_mul_unchecked_small{
2456- ( $t: ty, $nonzero_type: ty, $nonzero_check_mul_for: ident) => {
2457- #[ kani:: proof_for_contract( <$t>:: unchecked_mul) ]
2458- pub fn $nonzero_check_mul_for( ) {
2459- let x: $nonzero_type = kani:: any( ) ;
2460- let y: $nonzero_type = kani:: any( ) ;
2461-
2462- unsafe {
2463- x. unchecked_mul( y) ;
2464- }
2465- }
2466- } ;
2467- }
24682452
24692453 macro_rules! nonzero_check_cmp {
24702454 ( $nonzero_type: ty, $nonzero_check_cmp_for: ident) => {
@@ -2483,110 +2467,6 @@ mod verify {
24832467 } ;
24842468 }
24852469
2486- macro_rules! check_mul_unchecked_intervals{
2487- ( $t: ty, $nonzero_type: ty, $nonzero_check_mul_for: ident, $min: expr, $max: expr) => {
2488- #[ kani:: proof_for_contract( <$t>:: unchecked_mul) ]
2489- pub fn $nonzero_check_mul_for( ) {
2490- let x = kani:: any:: <$t>( ) ;
2491- let y = kani:: any:: <$t>( ) ;
2492-
2493- kani:: assume( x != 0 && x >= $min && x <= $max) ;
2494- kani:: assume( y != 0 && y >= $min && y <= $max) ;
2495-
2496- let x = <$nonzero_type>:: new( x) . unwrap( ) ;
2497- let y = <$nonzero_type>:: new( y) . unwrap( ) ;
2498-
2499- unsafe {
2500- x. unchecked_mul( y) ;
2501- }
2502- }
2503- } ;
2504- }
2505-
2506- //Calls for i32
2507- check_mul_unchecked_intervals ! ( i32 , NonZeroI32 , check_mul_i32_small, NonZeroI32 :: new( -10i32 ) . unwrap( ) . into( ) , NonZeroI32 :: new( 10i32 ) . unwrap( ) . into( ) ) ;
2508- check_mul_unchecked_intervals ! ( i32 , NonZeroI32 , check_mul_i32_large_pos, NonZeroI32 :: new( i32 :: MAX - 1000i32 ) . unwrap( ) . into( ) , NonZeroI32 :: new( i32 :: MAX ) . unwrap( ) . into( ) ) ;
2509- check_mul_unchecked_intervals ! ( i32 , NonZeroI32 , check_mul_i32_large_neg, NonZeroI32 :: new( i32 :: MIN + 1000i32 ) . unwrap( ) . into( ) , NonZeroI32 :: new( i32 :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2510- check_mul_unchecked_intervals ! ( i32 , NonZeroI32 , check_mul_i32_edge_pos, NonZeroI32 :: new( i32 :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroI32 :: new( i32 :: MAX ) . unwrap( ) . into( ) ) ;
2511- check_mul_unchecked_intervals ! ( i32 , NonZeroI32 , check_mul_i32_edge_neg, NonZeroI32 :: new( i32 :: MIN / 2 ) . unwrap( ) . into( ) , NonZeroI32 :: new( i32 :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2512-
2513- //Calls for i64
2514- check_mul_unchecked_intervals ! ( i64 , NonZeroI64 , check_mul_i64_small, NonZeroI64 :: new( -10i64 ) . unwrap( ) . into( ) , NonZeroI64 :: new( 10i64 ) . unwrap( ) . into( ) ) ;
2515- check_mul_unchecked_intervals ! ( i64 , NonZeroI64 , check_mul_i64_large_pos, NonZeroI64 :: new( i64 :: MAX - 1000i64 ) . unwrap( ) . into( ) , NonZeroI64 :: new( i64 :: MAX ) . unwrap( ) . into( ) ) ;
2516- check_mul_unchecked_intervals ! ( i64 , NonZeroI64 , check_mul_i64_large_neg, NonZeroI64 :: new( i64 :: MIN + 1000i64 ) . unwrap( ) . into( ) , NonZeroI64 :: new( i64 :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2517- check_mul_unchecked_intervals ! ( i64 , NonZeroI64 , check_mul_i64_edge_pos, NonZeroI64 :: new( i64 :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroI64 :: new( i64 :: MAX ) . unwrap( ) . into( ) ) ;
2518- check_mul_unchecked_intervals ! ( i64 , NonZeroI64 , check_mul_i64_edge_neg, NonZeroI64 :: new( i64 :: MIN / 2 ) . unwrap( ) . into( ) , NonZeroI64 :: new( i64 :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2519-
2520- //calls for i128
2521- check_mul_unchecked_intervals ! ( i128 , NonZeroI128 , check_mul_i128_small, NonZeroI128 :: new( -10i128 ) . unwrap( ) . into( ) , NonZeroI128 :: new( 10i128 ) . unwrap( ) . into( ) ) ;
2522- check_mul_unchecked_intervals ! ( i128 , NonZeroI128 , check_mul_i128_large_pos, NonZeroI128 :: new( i128 :: MAX - 1000i128 ) . unwrap( ) . into( ) , NonZeroI128 :: new( i128 :: MAX ) . unwrap( ) . into( ) ) ;
2523- check_mul_unchecked_intervals ! ( i128 , NonZeroI128 , check_mul_i128_large_neg, NonZeroI128 :: new( i128 :: MIN + 1000i128 ) . unwrap( ) . into( ) , NonZeroI128 :: new( i128 :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2524- check_mul_unchecked_intervals ! ( i128 , NonZeroI128 , check_mul_i128_edge_pos, NonZeroI128 :: new( i128 :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroI128 :: new( i128 :: MAX ) . unwrap( ) . into( ) ) ;
2525- check_mul_unchecked_intervals ! ( i128 , NonZeroI128 , check_mul_i128_edge_neg, NonZeroI128 :: new( i128 :: MIN / 2 ) . unwrap( ) . into( ) , NonZeroI128 :: new( i128 :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2526-
2527- //calls for isize
2528- check_mul_unchecked_intervals ! ( isize , NonZeroIsize , check_mul_isize_small, NonZeroIsize :: new( -10isize ) . unwrap( ) . into( ) , NonZeroIsize :: new( 10isize ) . unwrap( ) . into( ) ) ;
2529- check_mul_unchecked_intervals ! ( isize , NonZeroIsize , check_mul_isize_large_pos, NonZeroIsize :: new( isize :: MAX - 1000isize ) . unwrap( ) . into( ) , NonZeroIsize :: new( isize :: MAX ) . unwrap( ) . into( ) ) ;
2530- check_mul_unchecked_intervals ! ( isize , NonZeroIsize , check_mul_isize_large_neg, NonZeroIsize :: new( isize :: MIN + 1000isize ) . unwrap( ) . into( ) , NonZeroIsize :: new( isize :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2531- check_mul_unchecked_intervals ! ( isize , NonZeroIsize , check_mul_isize_edge_pos, NonZeroIsize :: new( isize :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroIsize :: new( isize :: MAX ) . unwrap( ) . into( ) ) ;
2532- check_mul_unchecked_intervals ! ( isize , NonZeroIsize , check_mul_isize_edge_neg, NonZeroIsize :: new( isize :: MIN / 2 ) . unwrap( ) . into( ) , NonZeroIsize :: new( isize :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2533-
2534- //calls for u32
2535- check_mul_unchecked_intervals ! ( u32 , NonZeroU32 , check_mul_u32_small, NonZeroU32 :: new( 1u32 ) . unwrap( ) . into( ) , NonZeroU32 :: new( 10u32 ) . unwrap( ) . into( ) ) ;
2536- check_mul_unchecked_intervals ! ( u32 , NonZeroU32 , check_mul_u32_large, NonZeroU32 :: new( u32 :: MAX - 1000u32 ) . unwrap( ) . into( ) , NonZeroU32 :: new( u32 :: MAX ) . unwrap( ) . into( ) ) ;
2537- check_mul_unchecked_intervals ! ( u32 , NonZeroU32 , check_mul_u32_edge, NonZeroU32 :: new( u32 :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroU32 :: new( u32 :: MAX ) . unwrap( ) . into( ) ) ;
2538-
2539- //calls for u64
2540- check_mul_unchecked_intervals ! ( u64 , NonZeroU64 , check_mul_u64_small, NonZeroU64 :: new( 1u64 ) . unwrap( ) . into( ) , NonZeroU64 :: new( 10u64 ) . unwrap( ) . into( ) ) ;
2541- check_mul_unchecked_intervals ! ( u64 , NonZeroU64 , check_mul_u64_large, NonZeroU64 :: new( u64 :: MAX - 1000u64 ) . unwrap( ) . into( ) , NonZeroU64 :: new( u64 :: MAX ) . unwrap( ) . into( ) ) ;
2542- check_mul_unchecked_intervals ! ( u64 , NonZeroU64 , check_mul_u64_edge, NonZeroU64 :: new( u64 :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroU64 :: new( u64 :: MAX ) . unwrap( ) . into( ) ) ;
2543-
2544- //calls for u128
2545- check_mul_unchecked_intervals ! ( u128 , NonZeroU128 , check_mul_u128_small, NonZeroU128 :: new( 1u128 ) . unwrap( ) . into( ) , NonZeroU128 :: new( 10u128 ) . unwrap( ) . into( ) ) ;
2546- check_mul_unchecked_intervals ! ( u128 , NonZeroU128 , check_mul_u128_large, NonZeroU128 :: new( u128 :: MAX - 1000u128 ) . unwrap( ) . into( ) , NonZeroU128 :: new( u128 :: MAX ) . unwrap( ) . into( ) ) ;
2547- check_mul_unchecked_intervals ! ( u128 , NonZeroU128 , check_mul_u128_edge, NonZeroU128 :: new( u128 :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroU128 :: new( u128 :: MAX ) . unwrap( ) . into( ) ) ;
2548-
2549- //calls for usize
2550- check_mul_unchecked_intervals ! ( usize , NonZeroUsize , check_mul_usize_small, NonZeroUsize :: new( 1usize ) . unwrap( ) . into( ) , NonZeroUsize :: new( 10usize ) . unwrap( ) . into( ) ) ;
2551- check_mul_unchecked_intervals ! ( usize , NonZeroUsize , check_mul_usize_large, NonZeroUsize :: new( usize :: MAX - 1000usize ) . unwrap( ) . into( ) , NonZeroUsize :: new( usize :: MAX ) . unwrap( ) . into( ) ) ;
2552- check_mul_unchecked_intervals ! ( usize , NonZeroUsize , check_mul_usize_edge, NonZeroUsize :: new( usize :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroUsize :: new( usize :: MAX ) . unwrap( ) . into( ) ) ;
2553-
2554- //calls for i8, i16, u8, u16
2555- check_mul_unchecked_small ! ( i8 , NonZeroI8 , nonzero_check_mul_for_i8) ;
2556- check_mul_unchecked_small ! ( i16 , NonZeroI16 , nonzero_check_mul_for_i16) ;
2557- check_mul_unchecked_small ! ( u8 , NonZeroU8 , nonzero_check_mul_for_u8) ;
2558- check_mul_unchecked_small ! ( u16 , NonZeroU16 , nonzero_check_mul_for_u16) ;
2559-
2560- //check_mul_unchecked_large!(i16, NonZeroU16, nonzero_check_mul_for_u16);
2561-
2562- macro_rules! nonzero_check_add {
2563- ( $t: ty, $nonzero_type: ty, $nonzero_check_unchecked_add_for: ident) => {
2564- #[ kani:: proof_for_contract( <$nonzero_type>:: unchecked_add) ]
2565- pub fn $nonzero_check_unchecked_add_for( ) {
2566- let x: $nonzero_type = kani:: any( ) ;
2567- let y: $t = kani:: any( ) ;
2568-
2569- unsafe {
2570- x. unchecked_add( y) ;
2571- }
2572- }
2573- } ;
2574- }
2575-
2576- // Generate proofs for all NonZero types
2577- nonzero_check_add ! ( i8 , core:: num:: NonZeroI8 , nonzero_check_unchecked_add_for_i8) ;
2578- nonzero_check_add ! ( i16 , core:: num:: NonZeroI16 , nonzero_check_unchecked_add_for_i16) ;
2579- nonzero_check_add ! ( i32 , core:: num:: NonZeroI32 , nonzero_check_unchecked_add_for_i32) ;
2580- nonzero_check_add ! ( i64 , core:: num:: NonZeroI64 , nonzero_check_unchecked_add_for_i64) ;
2581- nonzero_check_add ! ( i128 , core:: num:: NonZeroI128 , nonzero_check_unchecked_add_for_i128) ;
2582- nonzero_check_add ! ( isize , core:: num:: NonZeroIsize , nonzero_check_unchecked_add_for_isize) ;
2583- nonzero_check_add ! ( u8 , core:: num:: NonZeroU8 , nonzero_check_unchecked_add_for_u8) ;
2584- nonzero_check_add ! ( u16 , core:: num:: NonZeroU16 , nonzero_check_unchecked_add_for_u16) ;
2585- nonzero_check_add ! ( u32 , core:: num:: NonZeroU32 , nonzero_check_unchecked_add_for_u32) ;
2586- nonzero_check_add ! ( u64 , core:: num:: NonZeroU64 , nonzero_check_unchecked_add_for_u64) ;
2587- nonzero_check_add ! ( u128 , core:: num:: NonZeroU128 , nonzero_check_unchecked_add_for_u128) ;
2588- nonzero_check_add ! ( usize , core:: num:: NonZeroUsize , nonzero_check_unchecked_add_for_usize) ;
2589-
25902470 // Use the macro to generate different versions of the function for multiple types
25912471 nonzero_check_cmp ! ( core:: num:: NonZeroI8 , nonzero_check_cmp_for_i8) ;
25922472 nonzero_check_cmp ! ( core:: num:: NonZeroI16 , nonzero_check_cmp_for_i16) ;
@@ -2783,4 +2663,122 @@ mod verify {
27832663 nonzero_check_rotate_left_and_right ! ( core:: num:: NonZeroU64 , nonzero_check_rotate_for_u64) ;
27842664 nonzero_check_rotate_left_and_right ! ( core:: num:: NonZeroU128 , nonzero_check_rotate_for_u128) ;
27852665 nonzero_check_rotate_left_and_right ! ( core:: num:: NonZeroUsize , nonzero_check_rotate_for_usize) ;
2666+
2667+ macro_rules! check_mul_unchecked_small{
2668+ ( $t: ty, $nonzero_type: ty, $nonzero_check_mul_for: ident) => {
2669+ #[ kani:: proof_for_contract( <$t>:: unchecked_mul) ]
2670+ pub fn $nonzero_check_mul_for( ) {
2671+ let x: $nonzero_type = kani:: any( ) ;
2672+ let y: $nonzero_type = kani:: any( ) ;
2673+
2674+ unsafe {
2675+ x. unchecked_mul( y) ;
2676+ }
2677+ }
2678+ } ;
2679+ }
2680+
2681+ macro_rules! check_mul_unchecked_intervals{
2682+ ( $t: ty, $nonzero_type: ty, $nonzero_check_mul_for: ident, $min: expr, $max: expr) => {
2683+ #[ kani:: proof_for_contract( <$t>:: unchecked_mul) ]
2684+ pub fn $nonzero_check_mul_for( ) {
2685+ let x = kani:: any:: <$t>( ) ;
2686+ let y = kani:: any:: <$t>( ) ;
2687+
2688+ kani:: assume( x != 0 && x >= $min && x <= $max) ;
2689+ kani:: assume( y != 0 && y >= $min && y <= $max) ;
2690+
2691+ let x = <$nonzero_type>:: new( x) . unwrap( ) ;
2692+ let y = <$nonzero_type>:: new( y) . unwrap( ) ;
2693+
2694+ unsafe {
2695+ x. unchecked_mul( y) ;
2696+ }
2697+ }
2698+ } ;
2699+ }
2700+
2701+ //Calls for i32
2702+ check_mul_unchecked_intervals ! ( i32 , NonZeroI32 , check_mul_i32_small, NonZeroI32 :: new( -10i32 ) . unwrap( ) . into( ) , NonZeroI32 :: new( 10i32 ) . unwrap( ) . into( ) ) ;
2703+ check_mul_unchecked_intervals ! ( i32 , NonZeroI32 , check_mul_i32_large_pos, NonZeroI32 :: new( i32 :: MAX - 1000i32 ) . unwrap( ) . into( ) , NonZeroI32 :: new( i32 :: MAX ) . unwrap( ) . into( ) ) ;
2704+ check_mul_unchecked_intervals ! ( i32 , NonZeroI32 , check_mul_i32_large_neg, NonZeroI32 :: new( i32 :: MIN + 1000i32 ) . unwrap( ) . into( ) , NonZeroI32 :: new( i32 :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2705+ check_mul_unchecked_intervals ! ( i32 , NonZeroI32 , check_mul_i32_edge_pos, NonZeroI32 :: new( i32 :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroI32 :: new( i32 :: MAX ) . unwrap( ) . into( ) ) ;
2706+ check_mul_unchecked_intervals ! ( i32 , NonZeroI32 , check_mul_i32_edge_neg, NonZeroI32 :: new( i32 :: MIN / 2 ) . unwrap( ) . into( ) , NonZeroI32 :: new( i32 :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2707+
2708+ //Calls for i64
2709+ check_mul_unchecked_intervals ! ( i64 , NonZeroI64 , check_mul_i64_small, NonZeroI64 :: new( -10i64 ) . unwrap( ) . into( ) , NonZeroI64 :: new( 10i64 ) . unwrap( ) . into( ) ) ;
2710+ check_mul_unchecked_intervals ! ( i64 , NonZeroI64 , check_mul_i64_large_pos, NonZeroI64 :: new( i64 :: MAX - 1000i64 ) . unwrap( ) . into( ) , NonZeroI64 :: new( i64 :: MAX ) . unwrap( ) . into( ) ) ;
2711+ check_mul_unchecked_intervals ! ( i64 , NonZeroI64 , check_mul_i64_large_neg, NonZeroI64 :: new( i64 :: MIN + 1000i64 ) . unwrap( ) . into( ) , NonZeroI64 :: new( i64 :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2712+ check_mul_unchecked_intervals ! ( i64 , NonZeroI64 , check_mul_i64_edge_pos, NonZeroI64 :: new( i64 :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroI64 :: new( i64 :: MAX ) . unwrap( ) . into( ) ) ;
2713+ check_mul_unchecked_intervals ! ( i64 , NonZeroI64 , check_mul_i64_edge_neg, NonZeroI64 :: new( i64 :: MIN / 2 ) . unwrap( ) . into( ) , NonZeroI64 :: new( i64 :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2714+
2715+ //calls for i128
2716+ check_mul_unchecked_intervals ! ( i128 , NonZeroI128 , check_mul_i128_small, NonZeroI128 :: new( -10i128 ) . unwrap( ) . into( ) , NonZeroI128 :: new( 10i128 ) . unwrap( ) . into( ) ) ;
2717+ check_mul_unchecked_intervals ! ( i128 , NonZeroI128 , check_mul_i128_large_pos, NonZeroI128 :: new( i128 :: MAX - 1000i128 ) . unwrap( ) . into( ) , NonZeroI128 :: new( i128 :: MAX ) . unwrap( ) . into( ) ) ;
2718+ check_mul_unchecked_intervals ! ( i128 , NonZeroI128 , check_mul_i128_large_neg, NonZeroI128 :: new( i128 :: MIN + 1000i128 ) . unwrap( ) . into( ) , NonZeroI128 :: new( i128 :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2719+ check_mul_unchecked_intervals ! ( i128 , NonZeroI128 , check_mul_i128_edge_pos, NonZeroI128 :: new( i128 :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroI128 :: new( i128 :: MAX ) . unwrap( ) . into( ) ) ;
2720+ check_mul_unchecked_intervals ! ( i128 , NonZeroI128 , check_mul_i128_edge_neg, NonZeroI128 :: new( i128 :: MIN / 2 ) . unwrap( ) . into( ) , NonZeroI128 :: new( i128 :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2721+
2722+ //calls for isize
2723+ check_mul_unchecked_intervals ! ( isize , NonZeroIsize , check_mul_isize_small, NonZeroIsize :: new( -10isize ) . unwrap( ) . into( ) , NonZeroIsize :: new( 10isize ) . unwrap( ) . into( ) ) ;
2724+ check_mul_unchecked_intervals ! ( isize , NonZeroIsize , check_mul_isize_large_pos, NonZeroIsize :: new( isize :: MAX - 1000isize ) . unwrap( ) . into( ) , NonZeroIsize :: new( isize :: MAX ) . unwrap( ) . into( ) ) ;
2725+ check_mul_unchecked_intervals ! ( isize , NonZeroIsize , check_mul_isize_large_neg, NonZeroIsize :: new( isize :: MIN + 1000isize ) . unwrap( ) . into( ) , NonZeroIsize :: new( isize :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2726+ check_mul_unchecked_intervals ! ( isize , NonZeroIsize , check_mul_isize_edge_pos, NonZeroIsize :: new( isize :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroIsize :: new( isize :: MAX ) . unwrap( ) . into( ) ) ;
2727+ check_mul_unchecked_intervals ! ( isize , NonZeroIsize , check_mul_isize_edge_neg, NonZeroIsize :: new( isize :: MIN / 2 ) . unwrap( ) . into( ) , NonZeroIsize :: new( isize :: MIN + 1 ) . unwrap( ) . into( ) ) ;
2728+
2729+ //calls for u32
2730+ check_mul_unchecked_intervals ! ( u32 , NonZeroU32 , check_mul_u32_small, NonZeroU32 :: new( 1u32 ) . unwrap( ) . into( ) , NonZeroU32 :: new( 10u32 ) . unwrap( ) . into( ) ) ;
2731+ check_mul_unchecked_intervals ! ( u32 , NonZeroU32 , check_mul_u32_large, NonZeroU32 :: new( u32 :: MAX - 1000u32 ) . unwrap( ) . into( ) , NonZeroU32 :: new( u32 :: MAX ) . unwrap( ) . into( ) ) ;
2732+ check_mul_unchecked_intervals ! ( u32 , NonZeroU32 , check_mul_u32_edge, NonZeroU32 :: new( u32 :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroU32 :: new( u32 :: MAX ) . unwrap( ) . into( ) ) ;
2733+
2734+ //calls for u64
2735+ check_mul_unchecked_intervals ! ( u64 , NonZeroU64 , check_mul_u64_small, NonZeroU64 :: new( 1u64 ) . unwrap( ) . into( ) , NonZeroU64 :: new( 10u64 ) . unwrap( ) . into( ) ) ;
2736+ check_mul_unchecked_intervals ! ( u64 , NonZeroU64 , check_mul_u64_large, NonZeroU64 :: new( u64 :: MAX - 1000u64 ) . unwrap( ) . into( ) , NonZeroU64 :: new( u64 :: MAX ) . unwrap( ) . into( ) ) ;
2737+ check_mul_unchecked_intervals ! ( u64 , NonZeroU64 , check_mul_u64_edge, NonZeroU64 :: new( u64 :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroU64 :: new( u64 :: MAX ) . unwrap( ) . into( ) ) ;
2738+
2739+ //calls for u128
2740+ check_mul_unchecked_intervals ! ( u128 , NonZeroU128 , check_mul_u128_small, NonZeroU128 :: new( 1u128 ) . unwrap( ) . into( ) , NonZeroU128 :: new( 10u128 ) . unwrap( ) . into( ) ) ;
2741+ check_mul_unchecked_intervals ! ( u128 , NonZeroU128 , check_mul_u128_large, NonZeroU128 :: new( u128 :: MAX - 1000u128 ) . unwrap( ) . into( ) , NonZeroU128 :: new( u128 :: MAX ) . unwrap( ) . into( ) ) ;
2742+ check_mul_unchecked_intervals ! ( u128 , NonZeroU128 , check_mul_u128_edge, NonZeroU128 :: new( u128 :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroU128 :: new( u128 :: MAX ) . unwrap( ) . into( ) ) ;
2743+
2744+ //calls for usize
2745+ check_mul_unchecked_intervals ! ( usize , NonZeroUsize , check_mul_usize_small, NonZeroUsize :: new( 1usize ) . unwrap( ) . into( ) , NonZeroUsize :: new( 10usize ) . unwrap( ) . into( ) ) ;
2746+ check_mul_unchecked_intervals ! ( usize , NonZeroUsize , check_mul_usize_large, NonZeroUsize :: new( usize :: MAX - 1000usize ) . unwrap( ) . into( ) , NonZeroUsize :: new( usize :: MAX ) . unwrap( ) . into( ) ) ;
2747+ check_mul_unchecked_intervals ! ( usize , NonZeroUsize , check_mul_usize_edge, NonZeroUsize :: new( usize :: MAX / 2 ) . unwrap( ) . into( ) , NonZeroUsize :: new( usize :: MAX ) . unwrap( ) . into( ) ) ;
2748+
2749+ //calls for i8, i16, u8, u16
2750+ check_mul_unchecked_small ! ( i8 , NonZeroI8 , nonzero_check_mul_for_i8) ;
2751+ check_mul_unchecked_small ! ( i16 , NonZeroI16 , nonzero_check_mul_for_i16) ;
2752+ check_mul_unchecked_small ! ( u8 , NonZeroU8 , nonzero_check_mul_for_u8) ;
2753+ check_mul_unchecked_small ! ( u16 , NonZeroU16 , nonzero_check_mul_for_u16) ;
2754+
2755+ //check_mul_unchecked_large!(i16, NonZeroU16, nonzero_check_mul_for_u16);
2756+
2757+ macro_rules! nonzero_check_add {
2758+ ( $t: ty, $nonzero_type: ty, $nonzero_check_unchecked_add_for: ident) => {
2759+ #[ kani:: proof_for_contract( <$nonzero_type>:: unchecked_add) ]
2760+ pub fn $nonzero_check_unchecked_add_for( ) {
2761+ let x: $nonzero_type = kani:: any( ) ;
2762+ let y: $t = kani:: any( ) ;
2763+
2764+ unsafe {
2765+ x. unchecked_add( y) ;
2766+ }
2767+ }
2768+ } ;
2769+ }
2770+
2771+ // Generate proofs for all NonZero types
2772+ nonzero_check_add ! ( i8 , core:: num:: NonZeroI8 , nonzero_check_unchecked_add_for_i8) ;
2773+ nonzero_check_add ! ( i16 , core:: num:: NonZeroI16 , nonzero_check_unchecked_add_for_i16) ;
2774+ nonzero_check_add ! ( i32 , core:: num:: NonZeroI32 , nonzero_check_unchecked_add_for_i32) ;
2775+ nonzero_check_add ! ( i64 , core:: num:: NonZeroI64 , nonzero_check_unchecked_add_for_i64) ;
2776+ nonzero_check_add ! ( i128 , core:: num:: NonZeroI128 , nonzero_check_unchecked_add_for_i128) ;
2777+ nonzero_check_add ! ( isize , core:: num:: NonZeroIsize , nonzero_check_unchecked_add_for_isize) ;
2778+ nonzero_check_add ! ( u8 , core:: num:: NonZeroU8 , nonzero_check_unchecked_add_for_u8) ;
2779+ nonzero_check_add ! ( u16 , core:: num:: NonZeroU16 , nonzero_check_unchecked_add_for_u16) ;
2780+ nonzero_check_add ! ( u32 , core:: num:: NonZeroU32 , nonzero_check_unchecked_add_for_u32) ;
2781+ nonzero_check_add ! ( u64 , core:: num:: NonZeroU64 , nonzero_check_unchecked_add_for_u64) ;
2782+ nonzero_check_add ! ( u128 , core:: num:: NonZeroU128 , nonzero_check_unchecked_add_for_u128) ;
2783+ nonzero_check_add ! ( usize , core:: num:: NonZeroUsize , nonzero_check_unchecked_add_for_usize) ;
27862784}
0 commit comments