merge: sync upstream aeyakovenko/percolator v12.1 (136 commits)

Cargo.toml

@@ -23,7 +23,7 @@ test = []    # Use MAX_ACCOUNTS=64 (~0.17 SOL rent)
 small = []   # Use MAX_ACCOUNTS=256 (~0.68 SOL rent)
 medium = []  # Use MAX_ACCOUNTS=1024 (~2.7 SOL rent)
 # No feature = MAX_ACCOUNTS=4096 (~6.9 SOL rent)
-fuzz = []    # Enable fuzzing tests
+fuzz = ["test"]  # Enable fuzzing tests (includes test feature for test_visible helpers)
 
 [profile.release]
 lto = "fat"

scripts/run_kani_full_audit.sh

@@ -6,7 +6,8 @@ cd /home/anatoly/percolator
 OUTFILE="/home/anatoly/percolator/kani_audit_full.tsv"
 echo -e "proof\ttime_s\tstatus" > "$OUTFILE"
 
-PROOFS=$(grep -A5 'kani::proof' tests/kani.rs | grep '^\s*fn ' | sed 's/.*fn \([a-z_0-9]*\).*/\1/' | sort)
+# Collect all proof harness names from all proof files
+PROOFS=$(grep -rh '#\[kani::proof\]' tests/proofs_*.rs -A 3 | grep '^\s*fn ' | sed 's/.*fn \([a-z_0-9]*\).*/\1/' | sort -u)
 
 TOTAL=$(echo "$PROOFS" | wc -l)
 COUNT=0
@@ -18,7 +19,7 @@ for proof in $PROOFS; do
     echo "[$COUNT/$TOTAL] Running: $proof"
     START=$(date +%s)
 
-    if timeout 600 cargo kani --harness "$proof" --output-format terse 2>&1 | tail -3; then
+    if timeout 600 cargo kani --tests --harness "$proof" --output-format terse 2>&1 | tail -3; then
         STATUS="PASS"
         PASS=$((PASS + 1))
     else

src/wide_math.rs

@@ -252,7 +252,12 @@ impl U256 {
     /// Create from low 128 bits and high 128 bits.
     #[inline]
     pub const fn new(lo: u128, hi: u128) -> Self {
-        Self([lo as u64, (lo >> 64) as u64, hi as u64, (hi >> 64) as u64])
+        Self([
+            lo as u64,
+            (lo >> 64) as u64,
+            hi as u64,
+            (hi >> 64) as u64,
+        ])
     }
 
     #[inline]
@@ -867,7 +872,12 @@ impl I256 {
     }
 
     fn from_lo_hi(lo: u128, hi: u128) -> Self {
-        Self([lo as u64, (lo >> 64) as u64, hi as u64, (hi >> 64) as u64])
+        Self([
+            lo as u64,
+            (lo >> 64) as u64,
+            hi as u64,
+            (hi >> 64) as u64,
+        ])
     }
 
     fn as_raw_u256(self) -> U256 {
@@ -943,17 +953,18 @@ fn widening_mul_u128(a: u128, b: u128) -> (u128, u128) {
     let b_lo = b as u64 as u128;
     let b_hi = (b >> 64) as u64 as u128;
 
-    let ll = a_lo * b_lo; // 0..2^128
-    let lh = a_lo * b_hi; // 0..2^128
-    let hl = a_hi * b_lo; // 0..2^128
-    let hh = a_hi * b_hi; // 0..2^128
+    let ll = a_lo * b_lo;                  // 0..2^128
+    let lh = a_lo * b_hi;                  // 0..2^128
+    let hl = a_hi * b_lo;                  // 0..2^128
+    let hh = a_hi * b_hi;                  // 0..2^128
 
     // Accumulate:
     //   result = ll + (lh + hl) << 64 + hh << 128
     let (mid, mid_carry) = lh.overflowing_add(hl); // mid_carry means +2^128
 
     let (lo, lo_carry) = ll.overflowing_add(mid << 64);
-    let hi = hh + (mid >> 64) + ((mid_carry as u128) << 64) + (lo_carry as u128);
+    let hi = hh + (mid >> 64) + ((mid_carry as u128) << 64)
+           + (lo_carry as u128);
     // lo_carry is at most 1, captured in hi
 
     (lo, hi)
@@ -1100,7 +1111,6 @@ impl U512 {
     }
 
     /// Shift left by `bits`. Saturates to zero if bits >= 512.
-    #[allow(clippy::needless_range_loop)]
     fn shl_u512(self, bits: u32) -> Self {
         if bits >= 512 {
             return Self::ZERO;
@@ -1122,7 +1132,6 @@ impl U512 {
     }
 
     /// Shift right by `bits`.
-    #[allow(clippy::needless_range_loop)]
     fn shr_u512(self, bits: u32) -> Self {
         if bits >= 512 {
             return Self::ZERO;
@@ -1144,7 +1153,6 @@ impl U512 {
     }
 
     /// Subtract rhs from self. Assumes self >= rhs.
-    #[allow(clippy::needless_range_loop)]
     fn sub_u512(self, rhs: Self) -> Self {
         let mut result = [0u128; 4];
         let mut borrow = false;
@@ -1250,10 +1258,7 @@ impl U512 {
 /// Computes floor(n / d) where d > 0. Uses truncation toward zero, then
 /// adjusts: if n < 0 and there is a non-zero remainder, subtract 1.
 pub fn floor_div_signed_conservative(n: I256, d: U256) -> I256 {
-    assert!(
-        !d.is_zero(),
-        "floor_div_signed_conservative: zero denominator"
-    );
+    assert!(!d.is_zero(), "floor_div_signed_conservative: zero denominator");
 
     if n.is_zero() {
         return I256::ZERO;
@@ -1288,8 +1293,7 @@ pub fn floor_div_signed_conservative(n: I256, d: U256) -> I256 {
         let q_final = if r.is_zero() {
             q
         } else {
-            q.checked_add(U256::ONE)
-                .expect("floor_div quotient overflow")
+            q.checked_add(U256::ONE).expect("floor_div quotient overflow")
         };
 
         // Negate q_final to get the negative I256 result.
@@ -1303,26 +1307,27 @@ pub fn floor_div_signed_conservative(n: I256, d: U256) -> I256 {
     }
 }
 
-/// i128 version of floor_div_signed_conservative for compact code paths.
+/// Native i128 floor division: floor(n / d) for positive d, rounding toward
+/// negative infinity. Mirrors `floor_div_signed_conservative` but uses native
+/// i128/u128 arithmetic for the funding-term computation (spec §5.4).
 pub fn floor_div_signed_conservative_i128(n: i128, d: u128) -> i128 {
-    assert!(
-        d != 0,
-        "floor_div_signed_conservative_i128: zero denominator"
-    );
+    assert!(d != 0, "floor_div_signed_conservative_i128: zero denominator");
+
     if n == 0 {
         return 0;
     }
+
     if n > 0 {
+        // Non-negative: floor = truncation
         (n as u128 / d) as i128
     } else {
+        // Negative: floor(n/d) = -(|n| / d) - (if |n| % d != 0 then 1 else 0)
         let abs_n = n.unsigned_abs();
         let q = abs_n / d;
         let r = abs_n % d;
         let q_final = if r != 0 { q + 1 } else { q };
-        assert!(
-            q_final <= i128::MAX as u128,
-            "floor_div_signed_conservative_i128: result out of range"
-        );
+        assert!(q_final <= i128::MAX as u128,
+            "floor_div_signed_conservative_i128: result out of range");
         -(q_final as i128)
     }
 }
@@ -1352,10 +1357,7 @@ pub fn mul_div_floor_u256(a: U256, b: U256, d: U256) -> U256 {
 /// Like mul_div_floor_u256 but also returns the remainder.
 /// Returns (floor(a * b / d), (a * b) mod d).
 pub fn mul_div_floor_u256_with_rem(a: U256, b: U256, d: U256) -> (U256, U256) {
-    assert!(
-        !d.is_zero(),
-        "mul_div_floor_u256_with_rem: zero denominator"
-    );
+    assert!(!d.is_zero(), "mul_div_floor_u256_with_rem: zero denominator");
     let product = U512::mul_u256(a, b);
     product.div_rem_by_u256(d)
 }
@@ -1416,21 +1418,15 @@ pub fn fee_debt_u128_checked(fee_credits: i128) -> u128 {
 /// Uses the sign of `k_diff`. Computes `abs_basis * abs(k_diff)` as U512,
 /// then applies floor_div_signed_conservative logic.
 pub fn wide_signed_mul_div_floor(abs_basis: U256, k_diff: I256, denominator: U256) -> I256 {
-    assert!(
-        !denominator.is_zero(),
-        "wide_signed_mul_div_floor: zero denominator"
-    );
+    assert!(!denominator.is_zero(), "wide_signed_mul_div_floor: zero denominator");
 
     if k_diff.is_zero() || abs_basis.is_zero() {
         return I256::ZERO;
     }
 
     let negative = k_diff.is_negative();
     let abs_k = if negative {
-        assert!(
-            k_diff != I256::MIN,
-            "wide_signed_mul_div_floor: k_diff == I256::MIN"
-        );
+        assert!(k_diff != I256::MIN, "wide_signed_mul_div_floor: k_diff == I256::MIN");
         k_diff.abs_u256()
     } else {
         k_diff.abs_u256()
@@ -1448,15 +1444,13 @@ pub fn wide_signed_mul_div_floor(abs_basis: U256, k_diff: I256, denominator: U25
         let q_final = if r.is_zero() {
             q
         } else {
-            q.checked_add(U256::ONE)
-                .expect("wide_signed_mul_div_floor quotient overflow")
+            q.checked_add(U256::ONE).expect("wide_signed_mul_div_floor quotient overflow")
         };
         if q_final.is_zero() {
             I256::ZERO
         } else {
             let qi = I256::from_raw_u256(q_final);
-            qi.checked_neg()
-                .expect("wide_signed_mul_div_floor result out of I256 range")
+            qi.checked_neg().expect("wide_signed_mul_div_floor result out of I256 range")
         }
     }
 }
@@ -1473,7 +1467,7 @@ impl I256 {
 }
 
 // ============================================================================
-// §4.8 v11.5 Native 128-bit Arithmetic Helpers
+// §4.8 v11.31 Native 128-bit Arithmetic Helpers
 // ============================================================================
 
 /// Native multiply-divide floor. Product a*b must not overflow u128. Panics on d==0.
@@ -1488,48 +1482,33 @@ pub fn mul_div_ceil_u128(a: u128, b: u128, d: u128) -> u128 {
     assert!(d > 0, "mul_div_ceil_u128: division by zero");
     let p = a.checked_mul(b).expect("mul_div_ceil_u128: a*b overflow");
     let q = p / d;
-    if !p.is_multiple_of(d) {
-        q + 1
-    } else {
-        q
-    }
+    if p % d != 0 { q + 1 } else { q }
 }
 
 /// Exact wide multiply-divide floor using U256 intermediate.
 /// Used for haircut paths where a*b can exceed u128::MAX.
 pub fn wide_mul_div_floor_u128(a: u128, b: u128, d: u128) -> u128 {
     assert!(d > 0, "wide_mul_div_floor_u128: division by zero");
     let result = mul_div_floor_u256(U256::from_u128(a), U256::from_u128(b), U256::from_u128(d));
-    result
-        .try_into_u128()
-        .expect("wide_mul_div_floor_u128: result exceeds u128")
+    result.try_into_u128().expect("wide_mul_div_floor_u128: result exceeds u128")
 }
 
 /// Safe K-difference settlement (spec §4.8 lines 720-732).
 /// Computes K-difference in wide intermediate, then multiplies and divides.
-pub fn wide_signed_mul_div_floor_from_k_pair(
-    abs_basis: u128,
-    k_now: i128,
-    k_then: i128,
-    den: u128,
-) -> i128 {
+pub fn wide_signed_mul_div_floor_from_k_pair(abs_basis: u128, k_then: i128, k_now: i128, den: u128) -> i128 {
     assert!(den > 0, "wide_signed_mul_div_floor_from_k_pair: den == 0");
-    // Compute d = k_now - k_then in wide signed to avoid i128 overflow
+    // Compute d = k_now - k_then in wide signed to avoid i128 overflow (spec §4.8)
     let k_now_wide = I256::from_i128(k_now);
     let k_then_wide = I256::from_i128(k_then);
-    let d = k_now_wide
-        .checked_sub(k_then_wide)
-        .expect("K-diff overflow in wide");
+    let d = k_now_wide.checked_sub(k_then_wide).expect("K-diff overflow in wide");
     if d.is_zero() || abs_basis == 0 {
         return 0i128;
     }
     let abs_d = d.abs_u256();
     let abs_basis_u256 = U256::from_u128(abs_basis);
     let den_u256 = U256::from_u128(den);
     // p = abs_basis * abs(d), exact wide product
-    let p = abs_basis_u256
-        .checked_mul(abs_d)
-        .expect("wide product overflow");
+    let p = abs_basis_u256.checked_mul(abs_d).expect("wide product overflow");
     let (q, rem) = div_rem_u256(p, den_u256);
     if d.is_negative() {
         // mag = q + 1 if r != 0 else q
@@ -1539,17 +1518,11 @@ pub fn wide_signed_mul_div_floor_from_k_pair(
             q
         };
         let mag_u128 = mag.try_into_u128().expect("mag exceeds u128");
-        assert!(
-            mag_u128 <= i128::MAX as u128,
-            "wide_signed_mul_div_floor_from_k_pair: mag > i128::MAX"
-        );
+        assert!(mag_u128 <= i128::MAX as u128, "wide_signed_mul_div_floor_from_k_pair: mag > i128::MAX");
         -(mag_u128 as i128)
     } else {
         let q_u128 = q.try_into_u128().expect("quotient exceeds u128");
-        assert!(
-            q_u128 <= i128::MAX as u128,
-            "wide_signed_mul_div_floor_from_k_pair: q > i128::MAX"
-        );
+        assert!(q_u128 <= i128::MAX as u128, "wide_signed_mul_div_floor_from_k_pair: q > i128::MAX");
         q_u128 as i128
     }
 }
@@ -1560,15 +1533,8 @@ pub struct OverI128Magnitude;
 
 /// ADL delta_K representability check.
 /// Returns Ok(v) if the ceil result fits in i128 magnitude, Err otherwise.
-pub fn wide_mul_div_ceil_u128_or_over_i128max(
-    a: u128,
-    b: u128,
-    d: u128,
-) -> core::result::Result<u128, OverI128Magnitude> {
-    assert!(
-        d > 0,
-        "wide_mul_div_ceil_u128_or_over_i128max: division by zero"
-    );
+pub fn wide_mul_div_ceil_u128_or_over_i128max(a: u128, b: u128, d: u128) -> core::result::Result<u128, OverI128Magnitude> {
+    assert!(d > 0, "wide_mul_div_ceil_u128_or_over_i128max: division by zero");
     let result = mul_div_ceil_u256(U256::from_u128(a), U256::from_u128(b), U256::from_u128(d));
     match result.try_into_u128() {
         Some(v) if v <= i128::MAX as u128 => Ok(v),
@@ -1582,7 +1548,7 @@ pub fn saturating_mul_u128_u64(a: u128, b: u64) -> u128 {
         return 0;
     }
     let b128 = b as u128;
-    a.saturating_mul(b128)
+    a.checked_mul(b128).unwrap_or(u128::MAX)
 }
 
 // ============================================================================
@@ -1681,7 +1647,7 @@ mod tests {
     fn test_u256_mul_overflow() {
         let a = U256::new(0, 1); // 2^128
         let b = U256::new(0, 1); // 2^128
-                                 // Product would be 2^256, which overflows.
+        // Product would be 2^256, which overflows.
         assert_eq!(a.checked_mul(b), None);
     }
 
@@ -1883,15 +1849,9 @@ mod tests {
     #[test]
     fn test_ceil_div_positive() {
         // ceil(7 / 3) = 3
-        assert_eq!(
-            ceil_div_positive_checked(U256::from_u128(7), U256::from_u128(3)),
-            U256::from_u128(3)
-        );
+        assert_eq!(ceil_div_positive_checked(U256::from_u128(7), U256::from_u128(3)), U256::from_u128(3));
         // ceil(6 / 3) = 2
-        assert_eq!(
-            ceil_div_positive_checked(U256::from_u128(6), U256::from_u128(3)),
-            U256::from_u128(2)
-        );
+        assert_eq!(ceil_div_positive_checked(U256::from_u128(6), U256::from_u128(3)), U256::from_u128(2));
     }
 
     // --- saturating_mul_u256_u64 ---
@@ -2022,14 +1982,8 @@ mod tests {
     #[test]
     fn test_mul_div_max() {
         // MAX * 1 / 1 = MAX
-        assert_eq!(
-            mul_div_floor_u256(U256::MAX, U256::ONE, U256::ONE),
-            U256::MAX
-        );
+        assert_eq!(mul_div_floor_u256(U256::MAX, U256::ONE, U256::ONE), U256::MAX);
         // 1 * 1 / 1 = 1
-        assert_eq!(
-            mul_div_floor_u256(U256::ONE, U256::ONE, U256::ONE),
-            U256::ONE
-        );
+        assert_eq!(mul_div_floor_u256(U256::ONE, U256::ONE, U256::ONE), U256::ONE);
     }
 }