feat(contracts): implement overflow-safe math library with formal ver…

stellar-lend/Cargo.toml

@@ -13,6 +13,7 @@ members = [
   "contracts/lending-types",
   "contracts/lending-interest",
   "contracts/lending-risk",
+  "contracts/safe-math",
   "contracts/stablecoin",
   "contracts/institutional-wallet",
   "contracts/migration-hub",
@@ -21,12 +22,13 @@ members = [
   "contracts/privacy-pool",
   "contracts/reputation-system",
 ]
-exclude = ["fuzz"]
+exclude = ["fuzz", "formal-verification/safe-math-proofs"]
 
 [workspace.lints.rust]
 
 [workspace.dependencies]
 soroban-sdk = "23.4.1"
+stellarlend-safe-math = { path = "contracts/safe-math" }
 soroban-token-sdk = { version = "23.4.1" }
 serde = { version = "1.0", features = ["derive"] }
 serde_json = "1.0"

stellar-lend/contracts/lending-interest/Cargo.toml

@@ -9,9 +9,10 @@ crate-type = ["lib"]
 [dependencies]
 soroban-sdk = { workspace = true }
 lending-types = { path = "../lending-types" }
+stellarlend-safe-math = { workspace = true }
 
 [dev-dependencies]
-test-utils = { path = "../test-utils" }
+soroban-sdk = { workspace = true, features = ["testutils"] }
 
 [features]
 default = []

stellar-lend/contracts/lending-interest/src/lib.rs

@@ -1,6 +1,7 @@
 #![no_std]
 
 use soroban_sdk::Env;
+use stellarlend_safe_math::{bps_mul, safe_add, safe_div, safe_mul, MathError};
 
 pub struct InterestRateModel {
     pub base_rate: i128,
@@ -10,86 +11,145 @@ pub struct InterestRateModel {
 }
 
 impl InterestRateModel {
-    pub fn calculate_borrow_rate(&self, utilization: i128) -> i128 {
+    /// Variable-slope borrow rate in basis points.
+    ///
+    /// Below kink:  `base_rate + utilization × slope1 / 10 000`
+    /// Above kink:  `base_rate + kink × slope1 / 10 000 + excess × slope2 / 10 000`
+    pub fn calculate_borrow_rate(&self, utilization: i128) -> Result<i128, MathError> {
         if utilization <= self.optimal_utilization {
-            self.base_rate + (utilization * self.slope1 / 10_000)
+            let inc = safe_mul(utilization, self.slope1)
+                .and_then(|v| safe_div(v, 10_000))?;
+            safe_add(self.base_rate, inc)
         } else {
-            let excess = utilization - self.optimal_utilization;
-            self.base_rate + (self.optimal_utilization * self.slope1 / 10_000) + (excess * self.slope2 / 10_000)
+            let excess = safe_add(utilization, -self.optimal_utilization)?;
+            let kink_component = safe_mul(self.optimal_utilization, self.slope1)
+                .and_then(|v| safe_div(v, 10_000))?;
+            let excess_component = safe_mul(excess, self.slope2)
+                .and_then(|v| safe_div(v, 10_000))?;
+            safe_add(self.base_rate, kink_component)
+                .and_then(|v| safe_add(v, excess_component))
         }
     }
 
-    pub fn calculate_supply_rate(&self, borrow_rate: i128, utilization: i128, reserve_factor: i128) -> i128 {
-        let rate_to_pool = borrow_rate * (10_000 - reserve_factor) / 10_000;
-        rate_to_pool * utilization / 10_000
+    /// Supply rate: `borrow_rate × (10 000 − reserve_factor) / 10 000 × utilization / 10 000`
+    pub fn calculate_supply_rate(
+        &self,
+        borrow_rate: i128,
+        utilization: i128,
+        reserve_factor: i128,
+    ) -> Result<i128, MathError> {
+        let net_factor = safe_add(10_000, -reserve_factor)?;
+        let rate_to_pool = safe_mul(borrow_rate, net_factor)
+            .and_then(|v| safe_div(v, 10_000))?;
+        safe_mul(rate_to_pool, utilization).and_then(|v| safe_div(v, 10_000))
     }
 }
 
-pub fn calculate_utilization(total_borrows: i128, total_supply: i128) -> i128 {
+/// Utilization rate in basis points: `total_borrows × 10 000 / total_supply`.
+pub fn calculate_utilization(total_borrows: i128, total_supply: i128) -> Result<i128, MathError> {
     if total_supply == 0 {
-        return 0;
+        return Ok(0);
     }
-    total_borrows * 10_000 / total_supply
+    safe_mul(total_borrows, 10_000).and_then(|v| safe_div(v, total_supply))
 }
 
-pub fn accrue_interest(principal: i128, rate: i128, time_elapsed: u64) -> i128 {
+/// Simple interest via I256 intermediates: `principal × rate × elapsed / (SPY × 10 000)`.
+///
+/// Replaces the old `unwrap_or(0)` implementation which silently returned 0
+/// on overflow.  Now returns `Err(MathError::Overflow)` for very large inputs.
+pub fn accrue_interest(
+    env: &Env,
+    principal: i128,
+    rate: i128,
+    time_elapsed: u64,
+) -> Result<i128, MathError> {
     if time_elapsed == 0 {
-        return 0;
+        return Ok(0);
     }
-
-    let seconds_per_year = 31_536_000_i128;
-    principal
-        .checked_mul(rate)
-        .and_then(|v| v.checked_mul(time_elapsed as i128))
-        .and_then(|v| v.checked_div(seconds_per_year))
-        .and_then(|v| v.checked_div(10_000))
-        .unwrap_or(0)
+    stellarlend_safe_math::simple_interest(env, principal, rate, time_elapsed)
 }
 
-pub fn compound_interest(principal: i128, rate: i128, periods: u64) -> i128 {
+/// Compound interest over discrete periods using bps_mul for each step.
+pub fn compound_interest(principal: i128, rate: i128, periods: u64) -> Result<i128, MathError> {
     let mut result = principal;
     for _ in 0..periods {
-        let interest = result * rate / 10_000;
-        result = result.checked_add(interest).unwrap_or(result);
+        let interest = bps_mul(result, rate)?;
+        result = safe_add(result, interest)?;
     }
-    result - principal
+    safe_add(result, -principal)
 }
 
 #[cfg(test)]
 mod tests {
     use super::*;
+    use soroban_sdk::Env;
 
     #[test]
     fn test_utilization_calculation() {
-        assert_eq!(calculate_utilization(50_000, 100_000), 5_000);
-        assert_eq!(calculate_utilization(80_000, 100_000), 8_000);
-        assert_eq!(calculate_utilization(0, 100_000), 0);
-        assert_eq!(calculate_utilization(100_000, 0), 0);
+        assert_eq!(calculate_utilization(50_000, 100_000), Ok(5_000));
+        assert_eq!(calculate_utilization(80_000, 100_000), Ok(8_000));
+        assert_eq!(calculate_utilization(0, 100_000), Ok(0));
+        assert_eq!(calculate_utilization(100_000, 0), Ok(0));
     }
 
     #[test]
-    fn test_interest_rate_model() {
+    fn test_interest_rate_model_below_kink() {
         let model = InterestRateModel {
             base_rate: 200,
             slope1: 400,
             slope2: 6_000,
             optimal_utilization: 8_000,
         };
 
-        let rate_at_50 = model.calculate_borrow_rate(5_000);
+        let rate_at_50 = model.calculate_borrow_rate(5_000).unwrap();
         assert!(rate_at_50 > model.base_rate);
 
-        let rate_at_90 = model.calculate_borrow_rate(9_000);
+        let rate_at_90 = model.calculate_borrow_rate(9_000).unwrap();
         assert!(rate_at_90 > rate_at_50);
     }
 
     #[test]
-    fn test_accrue_interest() {
-        let principal = 100_000;
-        let rate = 500;
-        let time_elapsed = 31_536_000;
-
-        let interest = accrue_interest(principal, rate, time_elapsed);
+    fn test_accrue_interest_annual() {
+        let env = Env::default();
+        let interest = accrue_interest(&env, 100_000, 500, stellarlend_safe_math::SECONDS_PER_YEAR)
+            .unwrap();
         assert_eq!(interest, 5_000);
     }
+
+    #[test]
+    fn test_accrue_interest_zero_elapsed() {
+        let env = Env::default();
+        assert_eq!(accrue_interest(&env, 1_000_000, 500, 0), Ok(0));
+    }
+
+    #[test]
+    fn test_utilization_overflow_is_err() {
+        // total_borrows near MAX: safe_mul(MAX, 10_000) overflows.
+        let result = calculate_utilization(i128::MAX, 1);
+        assert!(result.is_err());
+    }
+
+    #[test]
+    fn test_borrow_rate_overflow_inputs_err() {
+        let model = InterestRateModel {
+            base_rate: i128::MAX,
+            slope1: i128::MAX,
+            slope2: i128::MAX,
+            optimal_utilization: 8_000,
+        };
+        assert!(model.calculate_borrow_rate(5_000).is_err());
+    }
+
+    #[test]
+    fn test_supply_rate_zero_pool() {
+        let model = InterestRateModel {
+            base_rate: 200,
+            slope1: 400,
+            slope2: 6_000,
+            optimal_utilization: 8_000,
+        };
+        // reserve_factor = 10_000 → net_factor = 0 → supply rate = 0.
+        let rate = model.calculate_supply_rate(500, 5_000, 10_000).unwrap();
+        assert_eq!(rate, 0);
+    }
 }

stellar-lend/contracts/safe-math/Cargo.toml

@@ -0,0 +1,18 @@
+[package]
+name = "stellarlend-safe-math"
+version = "0.1.0"
+edition = "2021"
+description = "Overflow-safe math library with formal verification proofs for StellarLend contracts"
+
+[lib]
+crate-type = ["rlib"]
+
+[dependencies]
+soroban-sdk = { workspace = true }
+
+[dev-dependencies]
+soroban-sdk = { workspace = true, features = ["testutils"] }
+proptest = { version = "1", default-features = false, features = ["alloc"] }
+
+[features]
+testutils = []

stellar-lend/contracts/safe-math/src/error.rs

@@ -0,0 +1,20 @@
+//! Error types for overflow-safe math operations.
+
+/// Errors that overflow-safe math operations can return.
+///
+/// Each variant corresponds to a distinct failure mode proven absent
+/// in the formal SMT specifications under `formal-verification/safe-math-proofs/`.
+#[derive(Copy, Clone, Debug, Eq, PartialEq, PartialOrd, Ord)]
+#[repr(u32)]
+pub enum MathError {
+    /// Arithmetic result exceeds i128::MAX.
+    Overflow = 1,
+    /// Arithmetic result is below i128::MIN (signed underflow).
+    Underflow = 2,
+    /// Divisor is zero.
+    DivisionByZero = 3,
+    /// Argument to sqrt is negative.
+    NegativeSqrt = 4,
+    /// Exponent too large; intermediate power would overflow.
+    ExponentTooLarge = 5,
+}