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.

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

Harnesses for carrying_mul #114

Merged
Merged
Changes from all commits
Commits
Show all changes
61 commits
Select commit Hold shift + click to select a range
1ae4c6d
Add Kani proofs of unchecked_add for all integer types
Sep 11, 2024
b553678
Format proof files & Add verification function templates
Sep 11, 2024
4db34e4
feat: add i8 uncheck shl verification
MWDZ Sep 11, 2024
54f5507
feat: add i16 and i32 uncheck shl verification
MWDZ Sep 11, 2024
472da0e
added unsafe integer i8 unchecked sub following the template
lanfeima Sep 12, 2024
daaaf7e
Experiment with two verification approaches in mod.rs of core::num
Sep 16, 2024
7bd0e3c
Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsa…
Yenyun035 Sep 18, 2024
1c9dbde
Add contracts to unchecked_add && Add i8::unchecked_add proof
Sep 18, 2024
894231f
Format core::num mod.rs
Sep 18, 2024
2bc4faf
Add comment for unchecked_add proofs
Sep 18, 2024
d9d4b5f
Add harnesses for i16,i32,i64,i128 unchecked_add
Sep 19, 2024
07c8b4a
Add harnesses for u8,u16,u32,u64,u128 unchecked_add
Sep 19, 2024
1fd4c6a
Cleanup misplaced proofs
Sep 19, 2024
b360311
Clean up comment
Sep 20, 2024
8cbca87
Format comment
Sep 20, 2024
0eef858
Remove before contracts. Fix import in
Sep 20, 2024
4858a53
Fix comment
Sep 20, 2024
8ce3381
Merge remote-tracking branch 'origin/c-0011-core-nums-yenyunw-unsafe-…
MWDZ Sep 23, 2024
bbd75f7
unchecked multiplication and shift right
rajathkotyal Sep 23, 2024
483bdf5
Merge branch 'main' into c-0011-core-nums-yenyunw-unsafe-ints
Yenyun035 Sep 23, 2024
71ffd37
Merge branch 'c-0011-core-nums-yenyunw-unsafe-ints' into c-0011-core-…
lanfeima Sep 23, 2024
a7d3cc2
feat: add contract and test case for unchecked_shl in type int and unit
MWDZ Sep 24, 2024
271afad
added preconditions and postconditions
lanfeima Sep 24, 2024
c7762c2
add proof functions for unchecked_sub
lanfeima Sep 24, 2024
ce35002
Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsa…
Yenyun035 Sep 24, 2024
d99844d
Remove ensures contracts && Undo formatting on existing code
Sep 24, 2024
fbcf49e
Add {isize, usize}::unchecked_add harnesses
Sep 24, 2024
864afa6
Small fix typo
rajathkotyal Sep 25, 2024
457a2b5
Merge branch 'model-checking:main' into c-0011-core-nums-yenyunw-unsa…
Yenyun035 Sep 27, 2024
54a03ef
Add harness generation macros for unchecked methods && Update uncheck…
Sep 27, 2024
ae678de
added limits to multiplication proofs, reduced duplicacy in code by u…
rajathkotyal Sep 29, 2024
af6942e
Merge branch 'c-0011-core-nums-yenyunw-unsafe-ints' into c-0011-core-…
rajathkotyal Sep 29, 2024
8ee5682
Remove unused import safety::ensures
Sep 30, 2024
02d706a
unchecked_mul and unchecked_shr proofs (#7)
rajathkotyal Sep 30, 2024
dce9e83
Add comments. Fix spacing
Sep 30, 2024
3880fc7
Revert "Add comments. Fix spacing"
rajathkotyal Oct 2, 2024
781cb87
Revert "unchecked_mul and unchecked_shr proofs (#7)"
rajathkotyal Oct 2, 2024
500e8db
Add comments. Fix spacing
rajathkotyal Oct 2, 2024
1c97825
cleaned up code: deleted the previous attempted proofs
lanfeima Oct 2, 2024
4572831
Merge branch 'c-0011-core-nums-yenyunw-unsafe-ints' into c-0011-core-…
lanfeima Oct 3, 2024
e3eb365
feat: merge the latest version
MWDZ Oct 3, 2024
2b3771f
feat: use macro rules for unchecked_shl harness
MWDZ Oct 3, 2024
1a3bf40
Merge branch 'c-0011-core-nums-junfengj-unchecked-shl' into c-0011-co…
MWDZ Oct 3, 2024
49b0a6b
add interval checks to unchecked_mul
rajathkotyal Oct 5, 2024
7118fa4
Merge branch 'main' into c-0011-core-nums-rajathm-unsafe-ints
rajathkotyal Oct 5, 2024
bbb9656
unchecked neg fix
rajathkotyal Oct 5, 2024
cafeea6
add missing i8, i16 unchecked_mul
rajathkotyal Oct 5, 2024
51745e0
Merge branch 'c-0011-core-nums-rajathm-unsafe-ints' into c-0011-core-…
lanfeima Oct 6, 2024
7f4421c
deleted the postconditions of unchecked_sub
lanfeima Oct 6, 2024
1331a77
deleted the postconditions for the unchecked_sub in uint_macros
lanfeima Oct 6, 2024
c413cac
refacted uncheck_sub harnesses
lanfeima Oct 6, 2024
8ce4a40
updated the branch with the main repository
lanfeima Oct 11, 2024
059dc02
Add carrying_mul verification harnesses for u8, u16, u32, and u64
lanfeima Oct 11, 2024
29ea0ce
updated the macro args for carrying_mult with initial carrying value
lanfeima Oct 11, 2024
6f7deae
resolved the compile error for carrying_mul
lanfeima Oct 15, 2024
ad031a1
deleted the kani submodule for merge
lanfeima Oct 15, 2024
ddabe95
formatted the style
lanfeima Oct 15, 2024
27522b4
Added documentation for generate_carrying_mul_intervals macro
lanfeima Oct 18, 2024
604d746
added full range interval for u8 and u16
lanfeima Oct 19, 2024
71399d8
reduced the interval for carrying_mul u32,u64
lanfeima Oct 20, 2024
1253264
Merge branch 'main' into c-0011-core-nums-lanfeim-carrying-mul
rajathkotyal Oct 25, 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
84 changes: 80 additions & 4 deletions library/core/src/num/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1657,6 +1657,51 @@ mod verify {
}
}
}

/// A macro to generate Kani proof harnesses for the `carrying_mul` method,
///
/// The macro creates multiple harnesses for different ranges of input values,
/// allowing testing of both small and large inputs.
///
/// # Parameters:
/// - `$type`: The integer type (e.g., u8, u16) for which the `carrying_mul` function is being tested.
/// - `$wide_type`: A wider type to simulate the multiplication (e.g., u16 for u8, u32 for u16).
/// - `$harness_name`: The name of the Kani harness to be generated.
/// - `$min`: The minimum value for the range of inputs for `lhs`, `rhs`, and `carry_in`.
/// - `$max`: The maximum value for the range of inputs for `lhs`, `rhs`, and `carry_in`.
macro_rules! generate_carrying_mul_intervals {
lanfeima marked this conversation as resolved.
Show resolved Hide resolved
($type:ty, $wide_type:ty, $($harness_name:ident, $min:expr, $max:expr),+) => {
$(
#[kani::proof]
pub fn $harness_name() {
let lhs: $type = kani::any::<$type>();
let rhs: $type = kani::any::<$type>();
let carry_in: $type = kani::any::<$type>();

kani::assume(lhs >= $min && lhs <= $max);
kani::assume(rhs >= $min && rhs <= $max);
kani::assume(carry_in >= $min && carry_in <= $max);

// Perform the carrying multiplication
let (result, carry_out) = lhs.carrying_mul(rhs, carry_in);

// Manually compute the expected result and carry using wider type
let wide_result = (lhs as $wide_type)
.wrapping_mul(rhs as $wide_type)
.wrapping_add(carry_in as $wide_type);

let expected_result = wide_result as $type;
let expected_carry = (wide_result >> <$type>::BITS) as $type;

// Assert the result and carry are correct
assert_eq!(result, expected_result);
assert_eq!(carry_out, expected_carry);
}
)+
}
}



// Part 2 : Nested unsafe functions Generation Macros --> https://github.com/verify-rust-std/blob/main/doc/src/challenges/0011-floats-ints.md

Expand Down Expand Up @@ -1741,7 +1786,7 @@ mod verify {
generate_unchecked_neg_harness!(i128, checked_unchecked_neg_i128);
generate_unchecked_neg_harness!(isize, checked_unchecked_neg_isize);

// unchecked_mul proofs
// `unchecked_mul` proofs
//
// Target types:
// i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total, with different interval checks for each.
Expand Down Expand Up @@ -1892,8 +1937,37 @@ mod verify {
generate_unchecked_math_harness!(u128, unchecked_sub, checked_unchecked_sub_u128);
generate_unchecked_math_harness!(usize, unchecked_sub, checked_unchecked_sub_usize);


// Part_2 `carrying_mul` proofs
//
// ====================== u8 Harnesses ======================
/// Kani proof harness for `carrying_mul` on `u8` type with full range of values.
generate_carrying_mul_intervals!(u8, u16,
carrying_mul_u8_full_range, 0u8, u8::MAX
);

// ====================== u16 Harnesses ======================
/// Kani proof harness for `carrying_mul` on `u16` type with full range of values.
generate_carrying_mul_intervals!(u16, u32,
carrying_mul_u16_full_range, 0u16, u16::MAX
);

// ====================== u32 Harnesses ======================
generate_carrying_mul_intervals!(u32, u64,
carrying_mul_u32_small, 0u32, 10u32,
carrying_mul_u32_large, u32::MAX - 10u32, u32::MAX,
carrying_mul_u32_mid_edge, (u32::MAX / 2) - 10u32, (u32::MAX / 2) + 10u32
);

// ====================== u64 Harnesses ======================
generate_carrying_mul_intervals!(u64, u128,
carrying_mul_u64_small, 0u64, 10u64,
carrying_mul_u64_large, u64::MAX - 10u64, u64::MAX,
carrying_mul_u64_mid_edge, (u64::MAX / 2) - 10u64, (u64::MAX / 2) + 10u64
);


// Part 2 : Proof harnesses
// Part_2 `widening_mul` proofs

// ====================== u8 Harnesses ======================
generate_widening_mul_intervals!(u8, u16, widening_mul_u8, 0u8, u8::MAX);
Expand All @@ -1919,7 +1993,7 @@ mod verify {
widening_mul_u64_mid_edge, (u64::MAX / 2) - 10u64, (u64::MAX / 2) + 10u64
);

// `wrapping_shl` proofs
// Part_2 `wrapping_shl` proofs
//
// Target types:
// i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
Expand All @@ -1944,7 +2018,7 @@ mod verify {
generate_wrapping_shift_harness!(u128, wrapping_shl, checked_wrapping_shl_u128);
generate_wrapping_shift_harness!(usize, wrapping_shl, checked_wrapping_shl_usize);

// `wrapping_shr` proofs
// Part_2 `wrapping_shr` proofs
//
// Target types:
// i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
Expand All @@ -1967,4 +2041,6 @@ mod verify {
generate_wrapping_shift_harness!(u64, wrapping_shr, checked_wrapping_shr_u64);
generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128);
generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize);

}

Loading