feat(settlement): add property-based test and document conservation i…

contracts/settlement/INVARIANTS.md

@@ -0,0 +1,32 @@
+# Conservation Invariant
+
+The fundamental conservation invariant of the Callora Settlement contract guarantees that the total amount of value received by the contract is always fully accounted for between the global pool and individual developer balances.
+
+## The Invariant
+
+`Sum of all payments received = Global Pool Balance + Sum of all Developer Balances`
+
+*Note: This invariant holds true in the absence of withdrawals. When withdrawals are considered, the invariant expands to:*
+`Sum of all payments received = Global Pool Balance + Sum of all Developer Balances + Sum of all Withdrawals`
+
+## Guarantees
+
+- **No Value Leakage**: Every unit of USDC (in micro-units) received from the Vault or Admin is credited either to the global pool or a specific developer.
+- **No Value Creation**: Credits cannot be generated out of thin air; they must originate from a `receive_payment` or `batch_receive_payment` call.
+- **Arithmetic Integrity**: Use of checked arithmetic ensures that balance overflows result in transaction failure rather than silent wrapping or loss of funds.
+
+## When It Holds
+
+The invariant holds after every successful transaction that modifies the settlement state. Specifically:
+- After `init`: both sides are 0.
+- After `receive_payment(to_pool=true)`: `Global Pool Balance` increases by `amount`.
+- After `receive_payment(to_pool=false)`: `Developer Balance` for a specific address increases by `amount`.
+- After `batch_receive_payment`: Multiple `Developer Balance` entries increase by their respective `amount` values.
+
+## Violations
+
+The invariant would be violated if:
+1. A credit is applied to a developer balance without being recorded in the total payments received.
+2. The global pool balance is modified without a corresponding payment.
+3. Arithmetic overflow occurs and is not caught (prevented by `checked_add`).
+4. Storage corruption or unauthorized direct storage modification occurs.

contracts/settlement/src/test.rs

@@ -1541,4 +1541,78 @@ mod settlement_tests {
             assert_eq!(client.get_developer_balance(dev), 1i128);
         }
     }
+
+    /// Property-based test that drives many randomized receive_payment calls
+    /// (mix of to_pool=true / false) and asserts the conservation invariant:
+    /// sum of all credits == pool total + sum of all developer balances.
+    /// Includes overflow-boundary cases near i128::MAX.
+    #[test]
+    fn test_conservation_invariant_randomized() {
+        let (env, addr, admin, vault, _third_party) = setup_contract();
+        let client = CalloraSettlementClient::new(&env, &addr);
+
+        let mut developers = std::vec::Vec::new();
+        for _ in 0..10 {
+            developers.push(Address::generate(&env));
+        }
+
+        let mut total_credited: i128 = 0;
+
+        // Simple deterministic pseudo-random generator
+        let mut seed: u128 = 42;
+        let mut next_rand = || {
+            seed = seed.wrapping_mul(1103515245).wrapping_add(12345);
+            seed
+        };
+
+        // 1. Run 100 randomized payments with small-to-medium amounts
+        for _ in 0..100 {
+            let to_pool = (next_rand() % 2) == 0;
+            let amount = (next_rand() % 1_000_000) as i128 + 1;
+
+            if to_pool {
+                client.receive_payment(&vault, &amount, &true, &None);
+            } else {
+                let dev_idx = (next_rand() % 10) as usize;
+                if let Some(developer) = developers.get(dev_idx) {
+                    client.receive_payment(&vault, &amount, &false, &Some(developer.clone()));
+                }
+            }
+            total_credited += amount;
+        }
+
+        // 2. Drive towards i128::MAX boundary
+        // Calculate remaining room to reach very close to i128::MAX
+        let buffer = 1_000_000_000_i128;
+        let remaining = i128::MAX - total_credited - buffer;
+
+        if remaining > 0 {
+            let half_remaining = remaining / 2;
+
+            // Large credit to pool
+            client.receive_payment(&vault, &half_remaining, &true, &None);
+            total_credited += half_remaining;
+
+            // Large credit to a developer
+            if let Some(developer) = developers.get(0) {
+                client.receive_payment(&vault, &half_remaining, &false, &Some(developer.clone()));
+                total_credited += half_remaining;
+            }
+        }
+
+        // Final Invariant Check
+        let pool = client.get_global_pool();
+        let mut sum_dev_balances: i128 = 0;
+
+        let all_balances = client.get_all_developer_balances(&admin);
+        for record in all_balances.iter() {
+            sum_dev_balances += record.balance;
+        }
+
+        assert_eq!(
+            total_credited,
+            pool.total_balance + sum_dev_balances,
+            "Conservation invariant violated: total credits must equal pool + developer balances"
+        );
+    }
 }