Add Kani formal verification harnesses and fix pre-existing clippy li…

.github/workflows/formal-verification.yml

@@ -0,0 +1,25 @@
+name: Formal Verification (Kani)
+
+on:
+  push:
+    branches: [main, dev]
+  pull_request:
+    branches: [main]
+
+env:
+  CARGO_TERM_COLOR: always
+
+jobs:
+  kani:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install Rust toolchain
+        uses: dtolnay/rust-toolchain@stable
+
+      - name: Install Kani
+        run: cargo install --locked kani-verifier && cargo kani setup
+
+      - name: Run all Kani proof harnesses
+        run: cargo kani

build.rs

@@ -0,0 +1,3 @@
+fn main() {
+    println!("cargo::rustc-check-cfg=cfg(kani)");
+}

src/access_control.rs

@@ -26,34 +26,34 @@ pub enum AccessControlKey {
 
 pub fn grant_role(env: Env, admin: Address, user: Address, role: Role) {
     admin.require_auth();
-    
+
     let stored_admin: Address = env
         .storage()
         .instance()
         .get(&AccessControlKey::Admin)
         .unwrap_or_else(|| panic!("not initialized"));
-    
+
     if admin != stored_admin {
         panic!("only admin can grant roles");
     }
-    
+
     let key = AccessControlKey::Role(user.clone());
     let role_data = RoleData {
         role: role.clone(),
         granted_at: env.ledger().timestamp(),
         granted_by: admin,
     };
-    
+
     env.storage().instance().set(&key, &role_data);
-    
+
     // Track role members
     let members_key = AccessControlKey::RoleMembers(role);
     let mut members: Vec<Address> = env
         .storage()
         .instance()
         .get(&members_key)
         .unwrap_or_else(|| Vec::new(&env));
-    
+
     if !members.contains(&user) {
         members.push_back(user);
         env.storage().instance().set(&members_key, &members);
@@ -62,23 +62,27 @@ pub fn grant_role(env: Env, admin: Address, user: Address, role: Role) {
 
 pub fn revoke_role(env: Env, admin: Address, user: Address) {
     admin.require_auth();
-    
+
     let stored_admin: Address = env
         .storage()
         .instance()
         .get(&AccessControlKey::Admin)
         .unwrap_or_else(|| panic!("not initialized"));
-    
+
     if admin != stored_admin {
         panic!("only admin can revoke roles");
     }
-    
+
     let key = AccessControlKey::Role(user.clone());
-    
+
     if let Some(role_data) = env.storage().instance().get::<_, RoleData>(&key) {
         // Remove from role members list
         let members_key = AccessControlKey::RoleMembers(role_data.role);
-        if let Some(mut members) = env.storage().instance().get::<_, Vec<Address>>(&members_key) {
+        if let Some(members) = env
+            .storage()
+            .instance()
+            .get::<_, Vec<Address>>(&members_key)
+        {
             let mut new_members = Vec::new(&env);
             for member in members.iter() {
                 if member != user {
@@ -87,7 +91,7 @@ pub fn revoke_role(env: Env, admin: Address, user: Address) {
             }
             env.storage().instance().set(&members_key, &new_members);
         }
-        
+
         env.storage().instance().remove(&key);
     }
 }

src/escrow.rs

@@ -51,7 +51,7 @@ pub fn create_milestone(
     let count_key = EscrowKey::MilestoneCount(task_id);
     let mut count: u32 = env.storage().persistent().get(&count_key).unwrap_or(0);
     count += 1;
-    
+
     let milestone = Milestone {
         id: count,
         task_id,
@@ -62,11 +62,11 @@ pub fn create_milestone(
         submission_url: None,
         feedback: None,
     };
-    
+
     let key = EscrowKey::Milestone(task_id, count);
     env.storage().persistent().set(&key, &milestone);
     env.storage().persistent().set(&count_key, &count);
-    
+
     count
 }
 
@@ -82,14 +82,15 @@ pub fn submit_milestone(
         .persistent()
         .get(&key)
         .unwrap_or_else(|| panic!("milestone not found"));
-
-    if milestone.status != MilestoneStatus::Pending && milestone.status != MilestoneStatus::Rejected {
+
+    if milestone.status != MilestoneStatus::Pending && milestone.status != MilestoneStatus::Rejected
+    {
         panic!("milestone cannot be submitted");
     }
-    
+
     milestone.status = MilestoneStatus::Submitted;
     milestone.submission_url = Some(submission_url);
-    
+
     env.storage().persistent().set(&key, &milestone);
 }
 
@@ -105,44 +106,39 @@ pub fn approve_milestone(
         .persistent()
         .get(&key)
         .unwrap_or_else(|| panic!("milestone not found"));
-    
+
     if milestone.status != MilestoneStatus::Submitted {
         panic!("milestone not submitted");
     }
-    
+
     milestone.status = MilestoneStatus::Approved;
     milestone.feedback = feedback;
-    
+
     let amount = milestone.amount;
-    
+
     env.storage().persistent().set(&key, &milestone);
-    
+
     // Update stats
     update_stats(&env, 0, amount, 0, 0, 0);
-    
+
     amount
 }
 
-pub fn reject_milestone(
-    env: Env,
-    task_id: u32,
-    milestone_id: u32,
-    feedback: soroban_sdk::String,
-) {
+pub fn reject_milestone(env: Env, task_id: u32, milestone_id: u32, feedback: soroban_sdk::String) {
     let key = EscrowKey::Milestone(task_id, milestone_id);
     let mut milestone: Milestone = env
         .storage()
         .persistent()
         .get(&key)
         .unwrap_or_else(|| panic!("milestone not found"));
-    
+
     if milestone.status != MilestoneStatus::Submitted {
         panic!("milestone not submitted");
     }
-    
+
     milestone.status = MilestoneStatus::Rejected;
     milestone.feedback = Some(feedback);
-    
+
     env.storage().persistent().set(&key, &milestone);
 }
 
@@ -154,14 +150,14 @@ pub fn get_milestone(env: Env, task_id: u32, milestone_id: u32) -> Option<Milest
 pub fn get_milestones_for_task(env: Env, task_id: u32) -> Vec<Milestone> {
     let count_key = EscrowKey::MilestoneCount(task_id);
     let count: u32 = env.storage().persistent().get(&count_key).unwrap_or(0);
-    
+
     let mut milestones = Vec::new(&env);
     for i in 1..=count {
         if let Some(milestone) = get_milestone(env.clone(), task_id, i) {
             milestones.push_back(milestone);
         }
     }
-    
+
     milestones
 }
 
@@ -174,24 +170,20 @@ pub fn update_stats(
     completed_delta: u32,
 ) {
     let key = EscrowKey::EscrowStats;
-    let mut stats: EscrowStats = env
-        .storage()
-        .persistent()
-        .get(&key)
-        .unwrap_or(EscrowStats {
-            total_locked: 0,
-            total_released: 0,
-            total_refunded: 0,
-            active_escrows: 0,
-            completed_escrows: 0,
-        });
-
+    let mut stats: EscrowStats = env.storage().persistent().get(&key).unwrap_or(EscrowStats {
+        total_locked: 0,
+        total_released: 0,
+        total_refunded: 0,
+        active_escrows: 0,
+        completed_escrows: 0,
+    });
+
     stats.total_locked += locked_delta;
     stats.total_released += released_delta;
     stats.total_refunded += refunded_delta;
     stats.active_escrows = (stats.active_escrows as i32 + active_delta as i32).max(0) as u32;
     stats.completed_escrows += completed_delta;
-    
+
     env.storage().persistent().set(&key, &stats);
 }
 
@@ -218,14 +210,14 @@ pub fn lock_escrow(env: Env, task_id: u32, amount: i128) {
 pub fn release_escrow(env: Env, task_id: u32, amount: i128) {
     let key = EscrowKey::TaskEscrow(task_id);
     let current: i128 = env.storage().persistent().get(&key).unwrap_or(0);
-    
+
     if current < amount {
         panic!("insufficient escrow balance");
     }
-    
+
     let new_balance = current - amount;
     env.storage().persistent().set(&key, &new_balance);
-    
+
     if new_balance == 0 {
         update_stats(&env, 0, amount, 0, 0, 1);
     } else {