From 7e52e12995fa04bfceebfe7094bd0e1e796a27ec Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Fri, 1 Aug 2025 12:40:05 -0700
Subject: [PATCH 01/18] 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: <https://nigeltao.github.io/blog/2020/parse-number-f64-simple.html>.
 
 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 <ntson@amazon.com>
Date: Fri, 1 Aug 2025 12:46:54 -0700
Subject: [PATCH 02/18] 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 <ntson@amazon.com>
Date: Fri, 1 Aug 2025 14:01:08 -0700
Subject: [PATCH 03/18] 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: <https://nigeltao.github.io/blog/2020/parse-number-f64-simple.html>.
 
-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 <ntson@amazon.com>
Date: Mon, 4 Aug 2025 07:47:20 -0700
Subject: [PATCH 04/18] Update library/core/src/num/dec2flt/decimal_seq.rs

Co-authored-by: Michael Tautschnig <mt@debian.org>
---
 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: <https://nigeltao.github.io/blog/2020/parse-number-f64-simple.html>.
 
+#[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 <ntson@amazon.com>
Date: Mon, 4 Aug 2025 07:47:29 -0700
Subject: [PATCH 05/18] Update library/core/src/num/dec2flt/decimal_seq.rs

Co-authored-by: Michael Tautschnig <mt@debian.org>
---
 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 <ntson@amazon.com>
Date: Mon, 4 Aug 2025 07:53:48 -0700
Subject: [PATCH 06/18] 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
         }

From 5753d41ed8129f09ce6720ad88c6db6226c50b64 Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Mon, 11 Aug 2025 10:42:05 -0700
Subject: [PATCH 07/18] change kaniindex to kani::index

---
 library/core/src/num/dec2flt/decimal_seq.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/core/src/num/dec2flt/decimal_seq.rs b/library/core/src/num/dec2flt/decimal_seq.rs
index 5b6147d0850cc..f87fc935fabe4 100644
--- a/library/core/src/num/dec2flt/decimal_seq.rs
+++ b/library/core/src/num/dec2flt/decimal_seq.rs
@@ -101,7 +101,7 @@ impl DecimalSeq {
         let dp = self.decimal_point as usize;
         let mut n = 0_u64;
 
-        #[kani::loop_invariant(n < 10u64.pow(kaniindex as u32))]
+        #[kani::loop_invariant(n < 10u64.pow(kani::index as u32))]
         for i in 0..dp {
             n *= 10;
             if i < self.num_digits {

From 5cd5a6cd11b87eb07ed6bba7cf6288f073663e99 Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Thu, 21 Aug 2025 13:16:27 -0700
Subject: [PATCH 08/18] add forall + change kani to safety

---
 library/core/src/num/dec2flt/decimal_seq.rs | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/library/core/src/num/dec2flt/decimal_seq.rs b/library/core/src/num/dec2flt/decimal_seq.rs
index f87fc935fabe4..652aead631df3 100644
--- a/library/core/src/num/dec2flt/decimal_seq.rs
+++ b/library/core/src/num/dec2flt/decimal_seq.rs
@@ -11,6 +11,8 @@
 
 #[cfg(kani)]
 use crate::kani;
+#[cfg(kani)]
+use crate::forall;
 use crate::num::dec2flt::common::{ByteSlice, is_8digits};
 
 /// A decimal floating-point number, represented as a sequence of decimal digits.
@@ -85,7 +87,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)]
+        #[safety::loop_invariant(self.num_digits <= Self::MAX_DIGITS)]
         while self.num_digits != 0 && self.digits[self.num_digits - 1] == 0 {
             self.num_digits -= 1;
         }
@@ -101,7 +103,7 @@ impl DecimalSeq {
         let dp = self.decimal_point as usize;
         let mut n = 0_u64;
 
-        #[kani::loop_invariant(n < 10u64.pow(kani::index as u32))]
+        #[safety::loop_invariant(n < 10u64.pow(kani::index as u32))]
         for i in 0..dp {
             n *= 10;
             if i < self.num_digits {
@@ -134,7 +136,7 @@ impl DecimalSeq {
         let mut write_index = self.num_digits + num_new_digits;
         let mut n = 0_u64;
 
-        #[kani::loop_invariant(read_index <= Self::MAX_DIGITS &&
+        #[safety::loop_invariant(read_index <= Self::MAX_DIGITS &&
             write_index == read_index + num_new_digits &&
             n < 10u64 << (shift - 1) &&
             self.num_digits <= Self::MAX_DIGITS &&
@@ -155,7 +157,7 @@ impl DecimalSeq {
             n = quotient;
         }
 
-        #[kani::loop_invariant(self.num_digits <= Self::MAX_DIGITS && self.decimal_point <= self.num_digits as i32)]
+        #[safety::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;
@@ -183,7 +185,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))]
+        #[safety::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;
@@ -191,7 +193,7 @@ impl DecimalSeq {
             } else if n == 0 {
                 return;
             } else {
-                #[kani::loop_invariant(n > 0 && read_index <= self.num_digits + 64 - n.leading_zeros() as usize && read_index > 0)]
+                #[safety::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;
@@ -208,7 +210,7 @@ impl DecimalSeq {
             return;
         }
         let mask = (1_u64 << shift) - 1;
-        #[kani::loop_invariant(self.num_digits <= Self::MAX_DIGITS &&
+        #[safety::loop_invariant(self.num_digits <= Self::MAX_DIGITS &&
             write_index < read_index &&
             write_index < Self::MAX_DIGITS - self.num_digits.saturating_sub(read_index)
         )]
@@ -219,7 +221,7 @@ impl DecimalSeq {
             self.digits[write_index] = new_digit;
             write_index += 1;
         }
-        #[kani::loop_invariant(write_index <= Self::MAX_DIGITS)]
+        #[safety::loop_invariant(write_index <= Self::MAX_DIGITS)]
         while n > 0 {
             let new_digit = (n >> shift) as u8;
             n = 10 * (n & mask);
@@ -382,7 +384,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)]
+    #[safety::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;

From 0ff0c95213dab197eabf57b3864bb886711dd7d2 Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Thu, 21 Aug 2025 13:27:37 -0700
Subject: [PATCH 09/18] fix format

---
 library/core/src/num/dec2flt/decimal_seq.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/core/src/num/dec2flt/decimal_seq.rs b/library/core/src/num/dec2flt/decimal_seq.rs
index 652aead631df3..18e973a472b98 100644
--- a/library/core/src/num/dec2flt/decimal_seq.rs
+++ b/library/core/src/num/dec2flt/decimal_seq.rs
@@ -9,10 +9,10 @@
 //! algorithm can be found in "ParseNumberF64 by Simple Decimal Conversion",
 //! available online: <https://nigeltao.github.io/blog/2020/parse-number-f64-simple.html>.
 
-#[cfg(kani)]
-use crate::kani;
 #[cfg(kani)]
 use crate::forall;
+#[cfg(kani)]
+use crate::kani;
 use crate::num::dec2flt::common::{ByteSlice, is_8digits};
 
 /// A decimal floating-point number, represented as a sequence of decimal digits.

From e8ac050839431f6ae833103ee29267de0e71e47b Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Thu, 21 Aug 2025 13:35:05 -0700
Subject: [PATCH 10/18] kani::forall -> forall

---
 library/core/src/num/dec2flt/decimal_seq.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/core/src/num/dec2flt/decimal_seq.rs b/library/core/src/num/dec2flt/decimal_seq.rs
index 18e973a472b98..1abc303e7d682 100644
--- a/library/core/src/num/dec2flt/decimal_seq.rs
+++ b/library/core/src/num/dec2flt/decimal_seq.rs
@@ -141,7 +141,7 @@ impl DecimalSeq {
             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)
+            forall!(|i in (0,DecimalSeq::MAX_DIGITS)| self.digits[i] <= 9)
         )]
         while read_index != 0 {
             read_index -= 1;
@@ -414,7 +414,7 @@ pub mod decimal_seq_verify {
                 digits: kani::any(),
             };
             kani::assume(ret.decimal_point <= ret.num_digits as i32);
-            kani::assume(kani::forall!(|i in (0,DecimalSeq::MAX_DIGITS)| ret.digits[i] <= 9));
+            kani::assume(forall!(|i in (0,DecimalSeq::MAX_DIGITS)| ret.digits[i] <= 9));
             ret
         }
     }

From f71ef69592d9d6e41563d0ca4a4ef501476bbce6 Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Thu, 21 Aug 2025 13:56:49 -0700
Subject: [PATCH 11/18] add -Z quantifier

---
 scripts/run-kani.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index b1aa9fe5e0e84..dfde1fccecec8 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -84,7 +84,7 @@ REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL}
 BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME}
 
 # Unstable arguments to pass to Kani
-unstable_args="-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z stubbing"
+unstable_args="-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing"
 
 # Variables used for parallel harness verification
 # When we say "parallel," we mean two dimensions of parallelization:

From f74f6e831bed5b971d27d918f0845983967ee50e Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Thu, 21 Aug 2025 14:52:02 -0700
Subject: [PATCH 12/18] add assumption

---
 library/core/src/num/dec2flt/decimal_seq.rs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/library/core/src/num/dec2flt/decimal_seq.rs b/library/core/src/num/dec2flt/decimal_seq.rs
index 1abc303e7d682..d2f35c09b5b73 100644
--- a/library/core/src/num/dec2flt/decimal_seq.rs
+++ b/library/core/src/num/dec2flt/decimal_seq.rs
@@ -159,6 +159,8 @@ impl DecimalSeq {
 
         #[safety::loop_invariant(self.num_digits <= Self::MAX_DIGITS && self.decimal_point <= self.num_digits as i32)]
         while n > 0 {
+            //true but hard to write proof with kani currently
+            kani::assume(write_index > 0);
             write_index -= 1;
             let quotient = n / 10;
             let remainder = n - (10 * quotient);

From ebe6aceedde3ca9f202fcf5c96e2cbd720ed35fa Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 22 Aug 2025 10:22:10 +0200
Subject: [PATCH 13/18] Update library/core/src/num/dec2flt/decimal_seq.rs

---
 library/core/src/num/dec2flt/decimal_seq.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/core/src/num/dec2flt/decimal_seq.rs b/library/core/src/num/dec2flt/decimal_seq.rs
index d2f35c09b5b73..d25f1b35a210a 100644
--- a/library/core/src/num/dec2flt/decimal_seq.rs
+++ b/library/core/src/num/dec2flt/decimal_seq.rs
@@ -157,10 +157,10 @@ impl DecimalSeq {
             n = quotient;
         }
 
-        #[safety::loop_invariant(self.num_digits <= Self::MAX_DIGITS && self.decimal_point <= self.num_digits as i32)]
+        #[safety::loop_invariant(self.num_digits <= Self::MAX_DIGITS && self.decimal_point <= self.num_digits as i32 && prev(write_index) > 0)]
         while n > 0 {
             //true but hard to write proof with kani currently
-            kani::assume(write_index > 0);
+            // kani::assume(write_index > 0);
             write_index -= 1;
             let quotient = n / 10;
             let remainder = n - (10 * quotient);

From 4559232e81c56573e342811072c8120aaea44278 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 22 Aug 2025 10:50:32 +0200
Subject: [PATCH 14/18] Update library/core/src/num/dec2flt/decimal_seq.rs

---
 library/core/src/num/dec2flt/decimal_seq.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/core/src/num/dec2flt/decimal_seq.rs b/library/core/src/num/dec2flt/decimal_seq.rs
index d25f1b35a210a..508d617fc294c 100644
--- a/library/core/src/num/dec2flt/decimal_seq.rs
+++ b/library/core/src/num/dec2flt/decimal_seq.rs
@@ -157,7 +157,7 @@ impl DecimalSeq {
             n = quotient;
         }
 
-        #[safety::loop_invariant(self.num_digits <= Self::MAX_DIGITS && self.decimal_point <= self.num_digits as i32 && prev(write_index) > 0)]
+        #[safety::loop_invariant(self.num_digits <= Self::MAX_DIGITS && self.decimal_point <= self.num_digits as i32 && (write_index > 0 || prev(write_index) == 1))]
         while n > 0 {
             //true but hard to write proof with kani currently
             // kani::assume(write_index > 0);

From c876cd6b96c362d38f66d5067e1d8f167e11fe9d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 22 Aug 2025 12:34:56 +0200
Subject: [PATCH 15/18] Update scripts/run-kani.sh

---
 scripts/run-kani.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index dfde1fccecec8..b1aa9fe5e0e84 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -84,7 +84,7 @@ REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL}
 BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME}
 
 # Unstable arguments to pass to Kani
-unstable_args="-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing"
+unstable_args="-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z stubbing"
 
 # Variables used for parallel harness verification
 # When we say "parallel," we mean two dimensions of parallelization:

From f9e0a67508ca3acbdff37c6908a2d4714ec12bc2 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 22 Aug 2025 10:38:56 +0000
Subject: [PATCH 16/18] Revert "Update scripts/run-kani.sh"

This reverts commit c876cd6b96c362d38f66d5067e1d8f167e11fe9d.
---
 scripts/run-kani.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index b1aa9fe5e0e84..dfde1fccecec8 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -84,7 +84,7 @@ REPO_URL=${KANI_REPO_URL:-$DEFAULT_REPO_URL}
 BRANCH_NAME=${KANI_BRANCH_NAME:-$DEFAULT_BRANCH_NAME}
 
 # Unstable arguments to pass to Kani
-unstable_args="-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z stubbing"
+unstable_args="-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing"
 
 # Variables used for parallel harness verification
 # When we say "parallel," we mean two dimensions of parallelization:

From b8b73bce7588c72e5180b88d4c3860e2e8528c7f Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 22 Aug 2025 10:42:32 +0000
Subject: [PATCH 17/18] write_index, again

---
 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 508d617fc294c..699ba2386be37 100644
--- a/library/core/src/num/dec2flt/decimal_seq.rs
+++ b/library/core/src/num/dec2flt/decimal_seq.rs
@@ -139,6 +139,7 @@ impl DecimalSeq {
         #[safety::loop_invariant(read_index <= Self::MAX_DIGITS &&
             write_index == read_index + num_new_digits &&
             n < 10u64 << (shift - 1) &&
+            (n == 0 || write_index > 0) &&
             self.num_digits <= Self::MAX_DIGITS &&
             self.decimal_point <= self.num_digits as i32 &&
             forall!(|i in (0,DecimalSeq::MAX_DIGITS)| self.digits[i] <= 9)

From 8ccd6934f1a82bc59dcb22a838497679297348f4 Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Fri, 22 Aug 2025 08:43:56 -0700
Subject: [PATCH 18/18] safety -> kani

---
 library/core/src/num/dec2flt/decimal_seq.rs | 22 ++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/library/core/src/num/dec2flt/decimal_seq.rs b/library/core/src/num/dec2flt/decimal_seq.rs
index 699ba2386be37..5c461873e81ed 100644
--- a/library/core/src/num/dec2flt/decimal_seq.rs
+++ b/library/core/src/num/dec2flt/decimal_seq.rs
@@ -87,7 +87,7 @@ impl DecimalSeq {
         //
         // Trim is only called in `right_shift` and `left_shift`.
         debug_assert!(self.num_digits <= Self::MAX_DIGITS);
-        #[safety::loop_invariant(self.num_digits <= Self::MAX_DIGITS)]
+        #[cfg_attr(kani, 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;
         }
@@ -103,7 +103,7 @@ impl DecimalSeq {
         let dp = self.decimal_point as usize;
         let mut n = 0_u64;
 
-        #[safety::loop_invariant(n < 10u64.pow(kani::index as u32))]
+        #[cfg_attr(kani, kani::loop_invariant(n < 10u64.pow(kani::index as u32)))]
         for i in 0..dp {
             n *= 10;
             if i < self.num_digits {
@@ -136,14 +136,14 @@ impl DecimalSeq {
         let mut write_index = self.num_digits + num_new_digits;
         let mut n = 0_u64;
 
-        #[safety::loop_invariant(read_index <= Self::MAX_DIGITS &&
+        #[cfg_attr(kani, kani::loop_invariant(read_index <= Self::MAX_DIGITS &&
             write_index == read_index + num_new_digits &&
             n < 10u64 << (shift - 1) &&
             (n == 0 || write_index > 0) &&
             self.num_digits <= Self::MAX_DIGITS &&
             self.decimal_point <= self.num_digits as i32 &&
             forall!(|i in (0,DecimalSeq::MAX_DIGITS)| self.digits[i] <= 9)
-        )]
+        ))]
         while read_index != 0 {
             read_index -= 1;
             write_index -= 1;
@@ -158,7 +158,7 @@ impl DecimalSeq {
             n = quotient;
         }
 
-        #[safety::loop_invariant(self.num_digits <= Self::MAX_DIGITS && self.decimal_point <= self.num_digits as i32 && (write_index > 0 || prev(write_index) == 1))]
+        #[cfg_attr(kani, kani::loop_invariant(self.num_digits <= Self::MAX_DIGITS && self.decimal_point <= self.num_digits as i32 && (write_index > 0 || prev(write_index) == 1)))]
         while n > 0 {
             //true but hard to write proof with kani currently
             // kani::assume(write_index > 0);
@@ -188,7 +188,7 @@ impl DecimalSeq {
         let mut read_index = 0;
         let mut write_index = 0;
         let mut n = 0_u64;
-        #[safety::loop_invariant( n == 0 || (read_index > 0 && read_index <= self.num_digits + 64 - n.leading_zeros() as usize))]
+        #[cfg_attr(kani, 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;
@@ -196,7 +196,7 @@ impl DecimalSeq {
             } else if n == 0 {
                 return;
             } else {
-                #[safety::loop_invariant(n > 0 && read_index <= self.num_digits + 64 - n.leading_zeros() as usize && read_index > 0)]
+                #[cfg_attr(kani, 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;
@@ -213,10 +213,10 @@ impl DecimalSeq {
             return;
         }
         let mask = (1_u64 << shift) - 1;
-        #[safety::loop_invariant(self.num_digits <= Self::MAX_DIGITS &&
+        #[cfg_attr(kani, 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;
@@ -224,7 +224,7 @@ impl DecimalSeq {
             self.digits[write_index] = new_digit;
             write_index += 1;
         }
-        #[safety::loop_invariant(write_index <= Self::MAX_DIGITS)]
+        #[cfg_attr(kani, kani::loop_invariant(write_index <= Self::MAX_DIGITS))]
         while n > 0 {
             let new_digit = (n >> shift) as u8;
             n = 10 * (n & mask);
@@ -387,7 +387,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..];
 
-    #[safety::loop_invariant(true)]
+    #[cfg_attr(kani, 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;