feat: add formal verification specs for interest rate model, oracle i…

.gitignore

@@ -58,6 +58,7 @@ stellar-lend/fuzz/coverage/
 
 # Test snapshots and coverage
 **/*.snap
+**/test_snapshots/
 **/coverage/
 **/.nyc_output/
 **/test-results/

docs/FORMAL_VERIFICATION.md

@@ -35,7 +35,15 @@ and are completely absent from the production WASM binary.
 | `spec::withdraw_spec` | `withdraw` | W-01 … W-07 |
 | `spec::protocol_invariants` | protocol accounting, health factor, interest index | P-01 ... P-05, H-01 ... H-05, I-01 ... I-03 |
 
-**Total: 69 lemmas across 9 critical function groups**
+| `spec::oracle_spec` | `get_price` � oracle data consumption paths | ORA-001 � ORA-010 |
+| `spec::cross_contract_spec` | Reentrancy, flash loans, AMM callbacks, migration atomicity | INV-REENTRANCY � INV-MIGRATION-COMPLETENESS |
+| `spec::upgrade_spec` | Upgrade state machine, storage safety | INV-UPGRADE-VERSION � INV-UPGRADE-ROLLBACK |
+| `spec::migration_hub` | Migration deadline, rate-limit, rollback | INV-MIG-DEADLINE � INV-MIG-ANALYTICS |
+| certora `interest_rate_model.spec` | IRM boundary conditions | IRM-001 � IRM-008 |
+| certora `oracle_integration.spec` | Oracle integration contracts | ORA-001 � ORA-010 |
+
+**Total: 69 lemmas across 9 critical function groups + 18 Certora rules across 2 new spec files + 4 new Rust spec modules**
+
 
 ---
 
@@ -227,3 +235,7 @@ The workflow at `.github/workflows/formal-verification.yml` runs:
 Kani is used as the Rust/Soroban model checker for this repository. It fills
 the same role that Certora Prover fills for Solidity/EVM projects while keeping
 the verification target native to the contract language used here.
+
+
+
+

docs/ORACLE_CONFIGURATION_GUIDE.md

@@ -457,6 +457,39 @@ contract.health_check()
    - Configuration issues
    - Resolution actions
 
+## Formal Verification
+
+The oracle integration contracts are covered by formal verification specifications to ensure correctness of critical oracle operations:
+
+### Certora Specifications
+
+The `stellar-lend/contracts/lending/certora/oracle_integration.spec` file defines machine-checkable specifications for oracle contract operations:
+
+- **ORA-001**: Price positivity — all reported prices must be strictly positive
+- **ORA-002**: Freeze blocks updates — oracle freeze state prevents price reporting
+- **ORA-003**: Unfreeze restores updates — unfreeze re-enables price reporting
+- **ORA-004**: Feed count monotonicity — registered feed count never decreases
+- **ORA-005**: Disable feed marks stale — disabled feeds are excluded from aggregation
+- **ORA-006**: Enable feed restores active — re-enabled feeds participate in aggregation
+- **ORA-007**: Staleness detection — prices exceeding `stale_threshold_seconds` are flagged
+- **ORA-008**: No active feeds error — `get_price` reverts when no feeds are available
+- **ORA-009**: Multiple feeds require active sources — aggregation needs at least one active feed
+- **ORA-010**: Feed count non-negative — feed registry count never goes below zero
+
+### Rust Property Tests
+
+The `contracts/lending/src/spec/oracle_spec.rs` module provides additional property-based tests for oracle data consumption paths within the lending contract.
+
+### Running Verification
+
+```bash
+# Run Certora specs (requires Certora Prover subscription)
+certoraRun stellar-lend/contracts/lending/certora/oracle_integration.spec
+
+# Run Rust property tests
+cargo test -p stellarlend-lending --features spec -- spec::oracle_spec
+```
+
 ## Conclusion
 
 Effective oracle configuration management is critical for the security and reliability of the StellarLend protocol. This guide provides the procedures and considerations necessary for maintaining a robust oracle system while ensuring proper role separation and security controls.

stellar-lend/contracts/lending/certora/interest_rate_model.spec

@@ -0,0 +1,186 @@
+// Formal Verification Specification for Interest Rate Model Boundary Conditions
+//
+// This document defines the formal verification specifications for the
+// InterestRateModel boundary conditions using the Certora Prover framework.
+//
+// Reference: Issue #865 - Formal Verification for Interest Rate Model Boundary Conditions
+
+methods {
+    function calculate_borrow_rate(i128) external returns (i128) envfree;
+    function calculate_supply_rate(i128, i128, i128) external returns (i128) envfree;
+    function calculate_utilization(i128, i128) external returns (i128) envfree;
+}
+
+// ============================================================================
+// IRM-001: Zero Utilization Borrow Rate
+// ============================================================================
+
+rule irm_001_zero_utilization_equals_base_rate(i128 base_rate, i128 slope1, i128 slope2, i128 optimal_utilization) {
+    require base_rate >= 0;
+    require slope1 >= 0;
+    require slope2 >= 0;
+    require optimal_utilization >= 0;
+    require optimal_utilization <= 10000;
+
+    int256 rate = calculate_borrow_rate(0);
+
+    assert rate == base_rate,
+        "IRM-001 VIOLATION: rate(0%) must equal base_rate exactly";
+}
+
+// ============================================================================
+// IRM-002: Full Utilization Borrow Rate is Maximum
+// ============================================================================
+
+rule irm_002_full_utilization_is_maximum(i128 base_rate, i128 slope1, i128 slope2, i128 optimal_utilization) {
+    require base_rate >= 0;
+    require slope1 >= 0;
+    require slope2 >= 0;
+    require optimal_utilization >= 0;
+    require optimal_utilization <= 10000;
+
+    int256 rate_at_zero = calculate_borrow_rate(0);
+    int256 rate_at_full = calculate_borrow_rate(10000);
+
+    assert rate_at_full >= rate_at_zero,
+        "IRM-002 VIOLATION: rate(100%) must be >= rate(0%)";
+}
+
+// ============================================================================
+// IRM-003: Monotonicity
+// ============================================================================
+
+rule irm_003_monotonicity(i128 base_rate, i128 slope1, i128 slope2, i128 optimal_utilization, i128 u1, i128 u2) {
+    require base_rate >= 0;
+    require slope1 >= 0;
+    require slope2 >= 0;
+    require optimal_utilization >= 0;
+    require optimal_utilization <= 10000;
+    require u1 >= 0;
+    require u1 <= 10000;
+    require u2 >= 0;
+    require u2 <= 10000;
+    require u1 <= u2;
+
+    int256 rate1 = calculate_borrow_rate(u1);
+    int256 rate2 = calculate_borrow_rate(u2);
+
+    assert rate1 <= rate2,
+        "IRM-003 VIOLATION: borrow rate must be monotonically non-decreasing in utilization";
+}
+
+// ============================================================================
+// IRM-004: Kink Continuity
+// ============================================================================
+
+rule irm_004_kink_continuity(i128 base_rate, i128 slope1, i128 slope2, i128 optimal_utilization) {
+    require base_rate >= 0;
+    require slope1 >= 0;
+    require slope2 >= 0;
+    require optimal_utilization >= 0;
+    require optimal_utilization <= 10000;
+
+    int256 at_kink = calculate_borrow_rate(optimal_utilization);
+
+    if (optimal_utilization < 10000) {
+        int256 just_above = calculate_borrow_rate(optimal_utilization + 1);
+
+        assert just_above >= at_kink,
+            "IRM-004 VIOLATION: rate must not decrease immediately above the kink";
+
+        assert just_above - at_kink <= (slope2 / 10000) + 1,
+            "IRM-004 VIOLATION: discontinuity at kink exceeds one slope2 step";
+    }
+}
+
+// ============================================================================
+// IRM-005: No Overflow for Realistic Parameters
+// ============================================================================
+
+rule irm_005_no_overflow(i128 base_rate, i128 slope1, i128 slope2, i128 optimal_utilization, i128 utilization) {
+    require base_rate >= 0;
+    require base_rate <= 1000000000000;
+    require slope1 >= 0;
+    require slope1 <= 1000000000000;
+    require slope2 >= 0;
+    require slope2 <= 1000000000000;
+    require optimal_utilization >= 0;
+    require optimal_utilization <= 10000;
+    require utilization >= 0;
+    require utilization <= 10000;
+
+    int256 result = calculate_borrow_rate(utilization);
+
+    assert result >= 0,
+        "IRM-005 VIOLATION: borrow rate must never be negative";
+}
+
+// ============================================================================
+// IRM-006: Supply Rate Bounds
+// ============================================================================
+
+rule irm_006_supply_rate_bounds(i128 base_rate, i128 slope1, i128 slope2, i128 optimal_utilization, i128 utilization, i128 reserve_factor) {
+    require base_rate >= 0;
+    require slope1 >= 0;
+    require slope2 >= 0;
+    require optimal_utilization >= 0;
+    require optimal_utilization <= 10000;
+    require utilization >= 0;
+    require utilization <= 10000;
+    require reserve_factor >= 0;
+    require reserve_factor <= 10000;
+
+    int256 borrow_rate = calculate_borrow_rate(utilization);
+    int256 supply_rate = calculate_supply_rate(borrow_rate, utilization, reserve_factor);
+
+    assert supply_rate >= 0,
+        "IRM-006 VIOLATION: supply rate must be non-negative";
+
+    assert supply_rate <= borrow_rate,
+        "IRM-006 VIOLATION: supply rate must not exceed borrow rate";
+}
+
+// ============================================================================
+// IRM-007: Utilization Calculation Correctness
+// ============================================================================
+
+rule irm_007_utilization_calculation(i128 total_borrows, i128 total_supply) {
+    require total_borrows >= 0;
+    require total_supply >= 0;
+
+    int256 utilization = calculate_utilization(total_borrows, total_supply);
+
+    if (total_supply == 0) {
+        assert utilization == 0,
+            "IRM-007 VIOLATION: utilization must be 0 when total_supply is 0";
+    } else {
+        assert utilization >= 0,
+            "IRM-007 VIOLATION: utilization must be non-negative";
+
+        assert utilization <= 10000,
+            "IRM-007 VIOLATION: utilization must not exceed 100%";
+    }
+}
+
+// ============================================================================
+// IRM-008: Rate Curve Area Sanity
+// ============================================================================
+
+rule irm_008_rate_curve_area_sanity(i128 base_rate, i128 slope1, i128 slope2, i128 optimal_utilization) {
+    require base_rate >= 0;
+    require slope1 >= 0;
+    require slope2 >= 0;
+    require optimal_utilization >= 0;
+    require optimal_utilization <= 10000;
+
+    int256 r0 = calculate_borrow_rate(0);
+    int256 r_kink = calculate_borrow_rate(optimal_utilization);
+    int256 r_max = calculate_borrow_rate(10000);
+
+    int256 area_below = (r0 + r_kink) * optimal_utilization / 2;
+    int256 area_above = (r_kink + r_max) * (10000 - optimal_utilization) / 2;
+    int256 expected_area = area_below + area_above;
+
+    assert expected_area >= 0,
+        "IRM-008 VIOLATION: area under rate curve must be non-negative";
+}