From 7e52e12995fa04bfceebfe7094bd0e1e796a27ec Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 1 Aug 2025 12:40:05 -0700 Subject: [PATCH 1/6] add loop invariants & harnesses for DecimalSeq functions --- library/core/src/num/dec2flt/decimal_seq.rs | 72 ++++++++++++++++++++- 1 file changed, 71 insertions(+), 1 deletion(-) diff --git a/library/core/src/num/dec2flt/decimal_seq.rs b/library/core/src/num/dec2flt/decimal_seq.rs index de22280c001c9..be1b84c4e5f92 100644 --- a/library/core/src/num/dec2flt/decimal_seq.rs +++ b/library/core/src/num/dec2flt/decimal_seq.rs @@ -10,6 +10,7 @@ //! available online: . use crate::num::dec2flt::common::{ByteSlice, is_8digits}; +use crate::kani; /// A decimal floating-point number, represented as a sequence of decimal digits. #[derive(Clone, Debug, PartialEq)] @@ -83,6 +84,7 @@ impl DecimalSeq { // // Trim is only called in `right_shift` and `left_shift`. debug_assert!(self.num_digits <= Self::MAX_DIGITS); + #[kani::loop_invariant(self.num_digits <= Self::MAX_DIGITS)] while self.num_digits != 0 && self.digits[self.num_digits - 1] == 0 { self.num_digits -= 1; } @@ -98,6 +100,7 @@ impl DecimalSeq { let dp = self.decimal_point as usize; let mut n = 0_u64; + #[kani::loop_invariant(n < 10u64.pow(kaniindex as u32))] for i in 0..dp { n *= 10; if i < self.num_digits { @@ -129,7 +132,14 @@ impl DecimalSeq { let mut read_index = self.num_digits; let mut write_index = self.num_digits + num_new_digits; let mut n = 0_u64; - + + #[kani::loop_invariant(read_index <= Self::MAX_DIGITS && + write_index == read_index + num_new_digits && + n < 10u64 << (shift - 1) && + self.num_digits <= Self::MAX_DIGITS && + self.decimal_point <= self.num_digits as i32 && + kani::forall!(|i in (0,DecimalSeq::MAX_DIGITS)| self.digits[i] <= 9) + )] while read_index != 0 { read_index -= 1; write_index -= 1; @@ -144,6 +154,7 @@ impl DecimalSeq { n = quotient; } + #[kani::loop_invariant(self.num_digits <= Self::MAX_DIGITS && self.decimal_point <= self.num_digits as i32)] while n > 0 { write_index -= 1; let quotient = n / 10; @@ -171,6 +182,7 @@ impl DecimalSeq { let mut read_index = 0; let mut write_index = 0; let mut n = 0_u64; + #[kani::loop_invariant( n == 0 || (read_index > 0 && read_index <= self.num_digits + 64 - n.leading_zeros() as usize))] while (n >> shift) == 0 { if read_index < self.num_digits { n = (10 * n) + self.digits[read_index] as u64; @@ -178,6 +190,8 @@ impl DecimalSeq { } else if n == 0 { return; } else { + kani::assume(read_index == self.num_digits); + #[kani::loop_invariant(n > 0 && read_index <= self.num_digits + 64 - n.leading_zeros() as usize && read_index > 0)] while (n >> shift) == 0 { n *= 10; read_index += 1; @@ -194,6 +208,10 @@ impl DecimalSeq { return; } let mask = (1_u64 << shift) - 1; + #[kani::loop_invariant(self.num_digits <= Self::MAX_DIGITS && + write_index < read_index && + write_index < Self::MAX_DIGITS - self.num_digits.saturating_sub(read_index) + )] while read_index < self.num_digits { let new_digit = (n >> shift) as u8; n = (10 * (n & mask)) + self.digits[read_index] as u64; @@ -201,6 +219,7 @@ impl DecimalSeq { self.digits[write_index] = new_digit; write_index += 1; } + #[kani::loop_invariant(write_index <= Self::MAX_DIGITS)] while n > 0 { let new_digit = (n >> shift) as u8; n = 10 * (n & mask); @@ -363,6 +382,7 @@ fn number_of_digits_decimal_left_shift(d: &DecimalSeq, mut shift: usize) -> usiz let pow5_b = (0x7FF & x_b) as usize; let pow5 = &TABLE_POW5[pow5_a..]; + #[kani::loop_invariant(true)] for (i, &p5) in pow5.iter().enumerate().take(pow5_b - pow5_a) { if i >= d.num_digits { return num_new_digits - 1; @@ -377,3 +397,53 @@ fn number_of_digits_decimal_left_shift(d: &DecimalSeq, mut shift: usize) -> usiz num_new_digits } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod decimal_seq_verify { + use super::*; + + impl kani::Arbitrary for DecimalSeq { + fn any() -> DecimalSeq { + let mut ret = DecimalSeq { + num_digits: kani::any(), + decimal_point: kani::any(), + truncated: kani::any(), + digits: kani::any() }; + kani::assume(a.num_digits <= DecimalSeq::MAX_DIGITS); + kani::assume(a.decimal_point>=0); + kani::assume(a.decimal_point <= a.num_digits as i32); + kani::assume(kani::forall!(|i in (0,DecimalSeq::MAX_DIGITS)| a.digits[i] <= 9)); + ret + } + } + + #[kani::proof] + fn check_round() { + let mut a: DecimalSeq = kani::any(); + a.round(); + } + + #[kani::proof] + fn check_number_of_digits_decimal_left_shift() { + let mut a: DecimalSeq = kani::any(); + let shift: usize = kani::any_where(|x| *x > 0 && *x <= 60); + let n = number_of_digits_decimal_left_shift(&a, shift); + assert!(n <= 19); + assert!(n == 19 || 1u64 << shift < 10u64.pow(n as u32 + 1)) + } + + #[kani::proof] + fn check_right_shift() { + let mut a: DecimalSeq = kani::any(); + let shift: usize = kani::any_where(|x| *x > 0 && *x <= 60); + a.right_shift(shift); + } + + #[kani::proof] + fn check_left_shift() { + let mut a: DecimalSeq = kani::any(); + let shift: usize = kani::any_where(|x| *x > 0 && *x <= 60); + a.left_shift(shift); + } +} From 1402d504bb7b167db6e883c78b0bb79e52a541cf Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 1 Aug 2025 12:46:54 -0700 Subject: [PATCH 2/6] remove unneccessary assume --- library/core/src/num/dec2flt/decimal_seq.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/library/core/src/num/dec2flt/decimal_seq.rs b/library/core/src/num/dec2flt/decimal_seq.rs index be1b84c4e5f92..4292a10e7339b 100644 --- a/library/core/src/num/dec2flt/decimal_seq.rs +++ b/library/core/src/num/dec2flt/decimal_seq.rs @@ -190,7 +190,6 @@ impl DecimalSeq { } else if n == 0 { return; } else { - kani::assume(read_index == self.num_digits); #[kani::loop_invariant(n > 0 && read_index <= self.num_digits + 64 - n.leading_zeros() as usize && read_index > 0)] while (n >> shift) == 0 { n *= 10; From 874421e7b9462f5ffb4af0ce40a7b01653ce5d3c Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 1 Aug 2025 14:01:08 -0700 Subject: [PATCH 3/6] fix format + add comments --- library/core/src/num/dec2flt/decimal_seq.rs | 24 ++++++++++++--------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/library/core/src/num/dec2flt/decimal_seq.rs b/library/core/src/num/dec2flt/decimal_seq.rs index 4292a10e7339b..25ce0329ad4fb 100644 --- a/library/core/src/num/dec2flt/decimal_seq.rs +++ b/library/core/src/num/dec2flt/decimal_seq.rs @@ -9,8 +9,8 @@ //! algorithm can be found in "ParseNumberF64 by Simple Decimal Conversion", //! available online: . -use crate::num::dec2flt::common::{ByteSlice, is_8digits}; use crate::kani; +use crate::num::dec2flt::common::{ByteSlice, is_8digits}; /// A decimal floating-point number, represented as a sequence of decimal digits. #[derive(Clone, Debug, PartialEq)] @@ -132,9 +132,9 @@ impl DecimalSeq { let mut read_index = self.num_digits; let mut write_index = self.num_digits + num_new_digits; let mut n = 0_u64; - - #[kani::loop_invariant(read_index <= Self::MAX_DIGITS && - write_index == read_index + num_new_digits && + + #[kani::loop_invariant(read_index <= Self::MAX_DIGITS && + write_index == read_index + num_new_digits && n < 10u64 << (shift - 1) && self.num_digits <= Self::MAX_DIGITS && self.decimal_point <= self.num_digits as i32 && @@ -207,8 +207,8 @@ impl DecimalSeq { return; } let mask = (1_u64 << shift) - 1; - #[kani::loop_invariant(self.num_digits <= Self::MAX_DIGITS && - write_index < read_index && + #[kani::loop_invariant(self.num_digits <= Self::MAX_DIGITS && + write_index < read_index && write_index < Self::MAX_DIGITS - self.num_digits.saturating_sub(read_index) )] while read_index < self.num_digits { @@ -408,13 +408,14 @@ pub mod decimal_seq_verify { num_digits: kani::any(), decimal_point: kani::any(), truncated: kani::any(), - digits: kani::any() }; + digits: kani::any(), + }; kani::assume(a.num_digits <= DecimalSeq::MAX_DIGITS); - kani::assume(a.decimal_point>=0); + kani::assume(a.decimal_point >= 0); kani::assume(a.decimal_point <= a.num_digits as i32); kani::assume(kani::forall!(|i in (0,DecimalSeq::MAX_DIGITS)| a.digits[i] <= 9)); - ret - } + ret + } } #[kani::proof] @@ -428,6 +429,8 @@ pub mod decimal_seq_verify { let mut a: DecimalSeq = kani::any(); let shift: usize = kani::any_where(|x| *x > 0 && *x <= 60); let n = number_of_digits_decimal_left_shift(&a, shift); + // 19 is the greatest number x such that 10u64^x does not overflow + // It is also TABLE.max << 11 assert!(n <= 19); assert!(n == 19 || 1u64 << shift < 10u64.pow(n as u32 + 1)) } @@ -435,6 +438,7 @@ pub mod decimal_seq_verify { #[kani::proof] fn check_right_shift() { let mut a: DecimalSeq = kani::any(); + //This function is called in parse_long_mantissa function (slow.rs), in which the maximum of shift is 60 let shift: usize = kani::any_where(|x| *x > 0 && *x <= 60); a.right_shift(shift); } From 13af0ca138d5c7e57bcc10ff2685cf3c35142e67 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 4 Aug 2025 07:47:20 -0700 Subject: [PATCH 4/6] Update library/core/src/num/dec2flt/decimal_seq.rs Co-authored-by: Michael Tautschnig --- library/core/src/num/dec2flt/decimal_seq.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/library/core/src/num/dec2flt/decimal_seq.rs b/library/core/src/num/dec2flt/decimal_seq.rs index 25ce0329ad4fb..91af1b914657c 100644 --- a/library/core/src/num/dec2flt/decimal_seq.rs +++ b/library/core/src/num/dec2flt/decimal_seq.rs @@ -9,6 +9,7 @@ //! algorithm can be found in "ParseNumberF64 by Simple Decimal Conversion", //! available online: . +#[cfg(kani)] use crate::kani; use crate::num::dec2flt::common::{ByteSlice, is_8digits}; From d2eb714f5ab1db48c7d4230fe5f84587292f74f0 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 4 Aug 2025 07:47:29 -0700 Subject: [PATCH 5/6] Update library/core/src/num/dec2flt/decimal_seq.rs Co-authored-by: Michael Tautschnig --- library/core/src/num/dec2flt/decimal_seq.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/library/core/src/num/dec2flt/decimal_seq.rs b/library/core/src/num/dec2flt/decimal_seq.rs index 91af1b914657c..41ae88931f0db 100644 --- a/library/core/src/num/dec2flt/decimal_seq.rs +++ b/library/core/src/num/dec2flt/decimal_seq.rs @@ -411,10 +411,10 @@ pub mod decimal_seq_verify { truncated: kani::any(), digits: kani::any(), }; - kani::assume(a.num_digits <= DecimalSeq::MAX_DIGITS); - kani::assume(a.decimal_point >= 0); - kani::assume(a.decimal_point <= a.num_digits as i32); - kani::assume(kani::forall!(|i in (0,DecimalSeq::MAX_DIGITS)| a.digits[i] <= 9)); + kani::assume(ret.num_digits <= DecimalSeq::MAX_DIGITS); + kani::assume(ret.decimal_point >= 0); + kani::assume(ret.decimal_point <= a.num_digits as i32); + kani::assume(kani::forall!(|i in (0,DecimalSeq::MAX_DIGITS)| ret.digits[i] <= 9)); ret } } From c8d98b39201b4242ab613f2379ad9e1f26d8af96 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 4 Aug 2025 07:53:48 -0700 Subject: [PATCH 6/6] fix impl Arbitrary --- library/core/src/num/dec2flt/decimal_seq.rs | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/library/core/src/num/dec2flt/decimal_seq.rs b/library/core/src/num/dec2flt/decimal_seq.rs index 41ae88931f0db..5b6147d0850cc 100644 --- a/library/core/src/num/dec2flt/decimal_seq.rs +++ b/library/core/src/num/dec2flt/decimal_seq.rs @@ -406,14 +406,12 @@ pub mod decimal_seq_verify { impl kani::Arbitrary for DecimalSeq { fn any() -> DecimalSeq { let mut ret = DecimalSeq { - num_digits: kani::any(), - decimal_point: kani::any(), + num_digits: kani::any_where(|x| *x <= DecimalSeq::MAX_DIGITS), + decimal_point: kani::any_where(|x| *x >= 0), truncated: kani::any(), digits: kani::any(), }; - kani::assume(ret.num_digits <= DecimalSeq::MAX_DIGITS); - kani::assume(ret.decimal_point >= 0); - kani::assume(ret.decimal_point <= a.num_digits as i32); + kani::assume(ret.decimal_point <= ret.num_digits as i32); kani::assume(kani::forall!(|i in (0,DecimalSeq::MAX_DIGITS)| ret.digits[i] <= 9)); ret }