diff --git a/contracts/xlm_wrapper/src/lib.rs b/contracts/xlm_wrapper/src/lib.rs
index f53016e..7f27f3f 100644
--- a/contracts/xlm_wrapper/src/lib.rs
+++ b/contracts/xlm_wrapper/src/lib.rs
@@ -27,6 +27,7 @@ pub enum DataKey {
     Name,
     Symbol,
     Decimals,
+    NativeAsset,
     Token,
     /// Tracks if an address is authorized to interact with AMM
     AMMAuthorized(Address),
@@ -48,7 +49,9 @@ impl XLMWrapper {
     /// * `admin` - Administrator address with special privileges
     /// * `name` - Token name (e.g., "Wrapped XLM")
     /// * `symbol` - Token symbol (e.g., "wXLM")
-    pub fn initialize(env: Env, admin: Address, token: Address, name: String, symbol: String) {
+    /// * `token` - Address of the wXLM token contract
+    /// * `native_asset` - Address of the native XLM token contract
+    pub fn initialize(env: Env, admin: Address, token: Address, name: String, symbol: String, native_asset: Address) {
         if env.storage().instance().has(&DataKey::Admin) {
             panic!("already initialized");
         }
@@ -60,6 +63,7 @@ impl XLMWrapper {
         env.storage().instance().set(&DataKey::Decimals, &7u32); // XLM uses 7 decimals
         env.storage().instance().set(&DataKey::Token, &token);
         env.storage().instance().set(&DataKey::Paused, &false);
+        env.storage().instance().set(&DataKey::NativeAsset, &native_asset);
         
         // Authorize the contract itself for AMM/Lending interactions
         let contract_addr = env.current_contract_address();
@@ -82,9 +86,9 @@ impl XLMWrapper {
         assert!(amount > 0, "amount must be positive");
         
         // Receive native XLM from user
+        let native_asset: Address = env.storage().instance().get(&DataKey::NativeAsset).expect("native asset not set");
         let contract_addr = env.current_contract_address();
-        let token_address: Address = env.storage().instance().get(&DataKey::Token).unwrap();
-        token::Client::new(&env, &token_address)
+        token::Client::new(&env, &native_asset)
             .transfer(&from, &contract_addr, &amount);
         
         // Mint wXLM to user (1:1 ratio)
@@ -132,9 +136,9 @@ impl XLMWrapper {
             .set(&DataKey::TotalSupply, &(supply - amount));
         
         // Send native XLM back to user
+        let native_asset: Address = env.storage().instance().get(&DataKey::NativeAsset).expect("native asset not set");
         let contract_addr = env.current_contract_address();
-        let token_address: Address = env.storage().instance().get(&DataKey::Token).unwrap();
-        token::Client::new(&env, &token_address)
+        token::Client::new(&env, &native_asset)
             .transfer(&contract_addr, &from, &amount);
         
         env.events()
@@ -165,6 +169,35 @@ impl XLMWrapper {
             .publish((symbol_short!("approve"), owner, spender), amount);
     }
 
+    /// Decrease the allowance granted to a spender
+    pub fn decrease_allowance(env: Env, owner: Address, spender: Address, amount: i128) {
+        owner.require_auth();
+        assert!(amount >= 0, "amount must be non-negative");
+        let current = Self::allowance(env.clone(), owner.clone(), spender.clone());
+        assert!(amount <= current, "insufficient allowance");
+        let new_allowance = current - amount;
+        env.storage().persistent().set(
+            &DataKey::Allowance(owner.clone(), spender.clone()),
+            &new_allowance,
+        );
+        env.events()
+            .publish((symbol_short!("dec_allow"), owner, spender), new_allowance);
+    }
+
+    /// Increase the allowance granted to a spender
+    pub fn increase_allowance(env: Env, owner: Address, spender: Address, amount: i128) {
+        owner.require_auth();
+        assert!(amount >= 0, "amount must be non-negative");
+        let current = Self::allowance(env.clone(), owner.clone(), spender.clone());
+        let new_allowance = current + amount;
+        env.storage().persistent().set(
+            &DataKey::Allowance(owner.clone(), spender.clone()),
+            &new_allowance,
+        );
+        env.events()
+            .publish((symbol_short!("inc_allow"), owner, spender), new_allowance);
+    }
+
     /// Set operator approval for all tokens
     pub fn set_approval_for_all(env: Env, owner: Address, operator: Address, approved: bool) {
         owner.require_auth();
@@ -431,12 +464,24 @@ impl XLMWrapper {
 mod tests {
     use super::*;
     use soroban_sdk::testutils::Address as _;
+    use soroban_sdk::token::StellarAssetClient;
+
+    struct TestEnv {
+        env: Env,
+        client: XLMWrapperClient<'static>,
+        sac: StellarAssetClient<'static>,
+        admin: Address,
+    }
 
-    fn setup() -> (Env, XLMWrapperClient<'static>, Address) {
+    fn setup() -> TestEnv {
         let env = Env::default();
         env.mock_all_auths();
         
         let admin = Address::generate(&env);
+        let sac_contract = env.register_stellar_asset_contract_v2(admin.clone());
+        let native_asset = sac_contract.address();
+        let sac = StellarAssetClient::new(&env, &native_asset);
+        
         let contract_id = env.register_contract(None, XLMWrapper);
         let client = XLMWrapperClient::new(&env, &contract_id);
         
@@ -446,183 +491,316 @@ mod tests {
             &token,
             &String::from_str(&env, "Wrapped XLM"),
             &String::from_str(&env, "wXLM"),
+            &native_asset,
         );
         
-        (env, client, admin)
+        TestEnv { env, client, sac, admin }
+    }
+
+    fn fund_user(te: &TestEnv, user: &Address, amount: i128) {
+        te.sac.mint(user, &amount);
     }
 
     #[test]
     fn test_initialize() {
-        let (env, client, admin) = setup();
+        let te = setup();
         
-        assert_eq!(client.name(), String::from_str(&env, "Wrapped XLM"));
-        assert_eq!(client.symbol(), String::from_str(&env, "wXLM"));
-        assert_eq!(client.decimals(), 7);
-        assert_eq!(client.total_supply(), 0);
+        assert_eq!(te.client.name(), String::from_str(&te.env, "Wrapped XLM"));
+        assert_eq!(te.client.symbol(), String::from_str(&te.env, "wXLM"));
+        assert_eq!(te.client.decimals(), 7);
+        assert_eq!(te.client.total_supply(), 0);
     }
 
     #[test]
     fn test_deposit_withdraw() {
-        let (env, client, admin) = setup();
-        let user = Address::generate(&env);
+        let te = setup();
+        let user = Address::generate(&te.env);
         
-        // Mock native XLM balance for testing
-        // In production, this would be actual native XLM
+        fund_user(&te, &user, 1000);
+        te.client.deposit(&user, &1000);
         
-        // Test deposit
-        let deposit_amount = 1000_i128;
-        client.deposit(&user, &deposit_amount);
+        assert_eq!(te.client.balance_of(&user), 1000);
+        assert_eq!(te.client.total_supply(), 1000);
         
-        assert_eq!(client.balance_of(&user), deposit_amount);
-        assert_eq!(client.total_supply(), deposit_amount);
+        te.client.withdraw(&user, &500);
         
-        // Test withdraw
-        let withdraw_amount = 500_i128;
-        client.withdraw(&user, &withdraw_amount);
-        
-        assert_eq!(client.balance_of(&user), deposit_amount - withdraw_amount);
-        assert_eq!(client.total_supply(), deposit_amount - withdraw_amount);
+        assert_eq!(te.client.balance_of(&user), 500);
+        assert_eq!(te.client.total_supply(), 500);
     }
 
     #[test]
     fn test_transfer() {
-        let (env, client, admin) = setup();
-        let alice = Address::generate(&env);
-        let bob = Address::generate(&env);
+        let te = setup();
+        let alice = Address::generate(&te.env);
+        let bob = Address::generate(&te.env);
         
-        client.deposit(&alice, &1000);
-        client.transfer(&alice, &bob, &300);
+        fund_user(&te, &alice, 1000);
+        te.client.deposit(&alice, &1000);
+        te.client.transfer(&alice, &bob, &300);
         
-        assert_eq!(client.balance_of(&alice), 700);
-        assert_eq!(client.balance_of(&bob), 300);
-        assert_eq!(client.total_supply(), 1000);
+        assert_eq!(te.client.balance_of(&alice), 700);
+        assert_eq!(te.client.balance_of(&bob), 300);
+        assert_eq!(te.client.total_supply(), 1000);
     }
 
     #[test]
     fn test_approve_and_transfer_from() {
-        let (env, client, admin) = setup();
-        let alice = Address::generate(&env);
-        let bob = Address::generate(&env);
-        let carol = Address::generate(&env);
+        let te = setup();
+        let alice = Address::generate(&te.env);
+        let bob = Address::generate(&te.env);
+        let carol = Address::generate(&te.env);
         
-        client.deposit(&alice, &1000);
-        client.approve(&alice, &bob, &500);
+        fund_user(&te, &alice, 1000);
+        te.client.deposit(&alice, &1000);
+        te.client.approve(&alice, &bob, &500);
         
-        assert_eq!(client.allowance(&alice, &bob), 500);
+        assert_eq!(te.client.allowance(&alice, &bob), 500);
         
-        client.transfer_from(&bob, &alice, &carol, &300);
+        te.client.transfer_from(&bob, &alice, &carol, &300);
         
-        assert_eq!(client.balance_of(&alice), 700);
-        assert_eq!(client.balance_of(&carol), 300);
-        assert_eq!(client.allowance(&alice, &bob), 200);
+        assert_eq!(te.client.balance_of(&alice), 700);
+        assert_eq!(te.client.balance_of(&carol), 300);
+        assert_eq!(te.client.allowance(&alice, &bob), 200);
+    }
+
+    #[test]
+    fn test_decrease_allowance() {
+        let te = setup();
+        let owner = Address::generate(&te.env);
+        let spender = Address::generate(&te.env);
+
+        fund_user(&te, &owner, 1000);
+        te.client.deposit(&owner, &1000);
+        te.client.approve(&owner, &spender, &500);
+
+        assert_eq!(te.client.allowance(&owner, &spender), 500);
+
+        te.client.decrease_allowance(&owner, &spender, &200);
+
+        assert_eq!(te.client.allowance(&owner, &spender), 300);
+    }
+
+    #[test]
+    fn test_decrease_allowance_to_zero() {
+        let te = setup();
+        let owner = Address::generate(&te.env);
+        let spender = Address::generate(&te.env);
+
+        fund_user(&te, &owner, 1000);
+        te.client.deposit(&owner, &1000);
+        te.client.approve(&owner, &spender, &300);
+        te.client.decrease_allowance(&owner, &spender, &300);
+
+        assert_eq!(te.client.allowance(&owner, &spender), 0);
+    }
+
+    #[test]
+    #[should_panic(expected = "insufficient allowance")]
+    fn test_decrease_allowance_exceeding_balance() {
+        let te = setup();
+        let owner = Address::generate(&te.env);
+        let spender = Address::generate(&te.env);
+
+        fund_user(&te, &owner, 1000);
+        te.client.deposit(&owner, &1000);
+        te.client.approve(&owner, &spender, &300);
+        te.client.decrease_allowance(&owner, &spender, &500);
+    }
+
+    #[test]
+    #[should_panic(expected = "insufficient allowance")]
+    fn test_decrease_allowance_from_zero() {
+        let te = setup();
+        let owner = Address::generate(&te.env);
+        let spender = Address::generate(&te.env);
+
+        fund_user(&te, &owner, 1000);
+        te.client.deposit(&owner, &1000);
+
+        // Decreasing from zero allowance should fail
+        te.client.decrease_allowance(&owner, &spender, &100);
+    }
+
+    #[test]
+    fn test_increase_allowance() {
+        let te = setup();
+        let owner = Address::generate(&te.env);
+        let spender = Address::generate(&te.env);
+
+        fund_user(&te, &owner, 1000);
+        te.client.deposit(&owner, &1000);
+        te.client.approve(&owner, &spender, &300);
+
+        assert_eq!(te.client.allowance(&owner, &spender), 300);
+
+        te.client.increase_allowance(&owner, &spender, &200);
+
+        assert_eq!(te.client.allowance(&owner, &spender), 500);
+    }
+
+    #[test]
+    fn test_increase_allowance_from_zero() {
+        let te = setup();
+        let owner = Address::generate(&te.env);
+        let spender = Address::generate(&te.env);
+
+        fund_user(&te, &owner, 1000);
+        te.client.deposit(&owner, &1000);
+
+        te.client.increase_allowance(&owner, &spender, &300);
+
+        assert_eq!(te.client.allowance(&owner, &spender), 300);
+    }
+
+    #[test]
+    #[should_panic(expected = "amount must be non-negative")]
+    fn test_decrease_allowance_negative_amount() {
+        let te = setup();
+        let owner = Address::generate(&te.env);
+        let spender = Address::generate(&te.env);
+
+        fund_user(&te, &owner, 1000);
+        te.client.deposit(&owner, &1000);
+        te.client.approve(&owner, &spender, &500);
+        te.client.decrease_allowance(&owner, &spender, &-100);
+    }
+
+    #[test]
+    fn test_allowance_combined_operations() {
+        let te = setup();
+        let owner = Address::generate(&te.env);
+        let spender = Address::generate(&te.env);
+
+        fund_user(&te, &owner, 1000);
+        te.client.deposit(&owner, &1000);
+
+        // Approve, then increase, then decrease, then transfer_from
+        te.client.approve(&owner, &spender, &200);
+        assert_eq!(te.client.allowance(&owner, &spender), 200);
+
+        te.client.increase_allowance(&owner, &spender, &100);
+        assert_eq!(te.client.allowance(&owner, &spender), 300);
+
+        te.client.decrease_allowance(&owner, &spender, &50);
+        assert_eq!(te.client.allowance(&owner, &spender), 250);
+
+        let recipient = Address::generate(&te.env);
+        te.client.transfer_from(&spender, &owner, &recipient, &100);
+        assert_eq!(te.client.allowance(&owner, &spender), 150);
+        assert_eq!(te.client.balance_of(&owner), 900);
+        assert_eq!(te.client.balance_of(&recipient), 100);
     }
 
     #[test]
     fn test_operator_approval() {
-        let (env, client, admin) = setup();
-        let alice = Address::generate(&env);
-        let operator = Address::generate(&env);
-        let bob = Address::generate(&env);
+        let te = setup();
+        let alice = Address::generate(&te.env);
+        let operator = Address::generate(&te.env);
+        let bob = Address::generate(&te.env);
         
-        client.deposit(&alice, &1000);
-        client.set_approval_for_all(&alice, &operator, &true);
+        fund_user(&te, &alice, 1000);
+        te.client.deposit(&alice, &1000);
+        te.client.set_approval_for_all(&alice, &operator, &true);
         
-        assert!(client.is_approved_for_all(&alice, &operator));
+        assert!(te.client.is_approved_for_all(&alice, &operator));
         
-        client.transfer_from(&operator, &alice, &bob, &300);
+        te.client.transfer_from(&operator, &alice, &bob, &300);
         
-        assert_eq!(client.balance_of(&alice), 700);
-        assert_eq!(client.balance_of(&bob), 300);
+        assert_eq!(te.client.balance_of(&alice), 700);
+        assert_eq!(te.client.balance_of(&bob), 300);
     }
 
     #[test]
     fn test_burn() {
-        let (env, client, admin) = setup();
-        let alice = Address::generate(&env);
+        let te = setup();
+        let alice = Address::generate(&te.env);
         
-        client.deposit(&alice, &1000);
-        client.burn(&alice, &300);
+        fund_user(&te, &alice, 1000);
+        te.client.deposit(&alice, &1000);
+        te.client.burn(&alice, &300);
         
-        assert_eq!(client.balance_of(&alice), 700);
-        assert_eq!(client.total_supply(), 700);
+        assert_eq!(te.client.balance_of(&alice), 700);
+        assert_eq!(te.client.total_supply(), 700);
     }
 
     #[test]
     fn test_amm_authorization() {
-        let (env, client, admin) = setup();
-        let amm_address = Address::generate(&env);
+        let te = setup();
+        let amm_address = Address::generate(&te.env);
         
-        assert!(!client.is_amm_authorized(&amm_address));
+        assert!(!te.client.is_amm_authorized(&amm_address));
         
-        client.authorize_amm(&admin, &amm_address);
-        assert!(client.is_amm_authorized(&amm_address));
+        te.client.authorize_amm(&te.admin, &amm_address);
+        assert!(te.client.is_amm_authorized(&amm_address));
         
-        client.revoke_amm(&admin, &amm_address);
-        assert!(!client.is_amm_authorized(&amm_address));
+        te.client.revoke_amm(&te.admin, &amm_address);
+        assert!(!te.client.is_amm_authorized(&amm_address));
     }
 
     #[test]
     fn test_lending_authorization() {
-        let (env, client, admin) = setup();
-        let lending_address = Address::generate(&env);
+        let te = setup();
+        let lending_address = Address::generate(&te.env);
         
-        assert!(!client.is_lending_authorized(&lending_address));
+        assert!(!te.client.is_lending_authorized(&lending_address));
         
-        client.authorize_lending(&admin, &lending_address);
-        assert!(client.is_lending_authorized(&lending_address));
+        te.client.authorize_lending(&te.admin, &lending_address);
+        assert!(te.client.is_lending_authorized(&lending_address));
         
-        client.revoke_lending(&admin, &lending_address);
-        assert!(!client.is_lending_authorized(&lending_address));
+        te.client.revoke_lending(&te.admin, &lending_address);
+        assert!(!te.client.is_lending_authorized(&lending_address));
     }
 
     #[test]
     fn test_pause_unpause() {
-        let (env, client, admin) = setup();
-        let user = Address::generate(&env);
+        let te = setup();
+        let user = Address::generate(&te.env);
         
-        assert!(!client.is_paused());
+        assert!(!te.client.is_paused());
         
-        client.pause(&admin);
-        assert!(client.is_paused());
+        te.client.pause(&te.admin);
+        assert!(te.client.is_paused());
         
-        client.unpause(&admin);
-        assert!(!client.is_paused());
+        te.client.unpause(&te.admin);
+        assert!(!te.client.is_paused());
     }
 
     #[test]
     #[should_panic(expected = "contract is paused")]
     fn test_deposit_when_paused() {
-        let (env, client, admin) = setup();
-        let user = Address::generate(&env);
+        let te = setup();
+        let user = Address::generate(&te.env);
         
-        client.pause(&admin);
-        client.deposit(&user, &1000);
+        te.client.pause(&te.admin);
+        te.client.deposit(&user, &1000);
     }
 
     #[test]
     #[should_panic(expected = "contract is paused")]
     fn test_withdraw_when_paused() {
-        let (env, client, admin) = setup();
-        let user = Address::generate(&env);
+        let te = setup();
+        let user = Address::generate(&te.env);
         
-        client.deposit(&user, &1000);
-        client.pause(&admin);
-        client.withdraw(&user, &500);
+        fund_user(&te, &user, 1000);
+        te.client.deposit(&user, &1000);
+        te.client.pause(&te.admin);
+        te.client.withdraw(&user, &500);
     }
 
     #[test]
     fn test_one_to_one_peg() {
-        let (env, client, admin) = setup();
-        let user = Address::generate(&env);
+        let te = setup();
+        let user = Address::generate(&te.env);
         
         // Verify 1:1 peg is maintained
-        client.deposit(&user, &1000);
-        assert_eq!(client.balance_of(&user), 1000);
-        assert_eq!(client.total_supply(), 1000);
+        fund_user(&te, &user, 1000);
+        te.client.deposit(&user, &1000);
+        assert_eq!(te.client.balance_of(&user), 1000);
+        assert_eq!(te.client.total_supply(), 1000);
         
-        client.withdraw(&user, &1000);
-        assert_eq!(client.balance_of(&user), 0);
-        assert_eq!(client.total_supply(), 0);
+        te.client.withdraw(&user, &1000);
+        assert_eq!(te.client.balance_of(&user), 0);
+        assert_eq!(te.client.total_supply(), 0);
     }
 }
 
@@ -637,12 +815,24 @@ mod invariants {
     extern crate std;
     use super::*;
     use soroban_sdk::testutils::Address as _;
+    use soroban_sdk::token::StellarAssetClient;
 
-    /// Helper to set up a fresh contract instance
-    fn setup_fresh() -> (Env, XLMWrapperClient<'static>, Address) {
+    fn fund_user(env: &Env, sac: &StellarAssetClient<'_>, user: &Address, amount: i128) {
+        sac.mint(user, &amount);
+    }
+
+    fn fund_and_deposit(env: &Env, sac: &StellarAssetClient<'_>, client: &XLMWrapperClient<'_>, user: &Address, amount: i128) {
+        fund_user(env, sac, user, amount);
+        client.deposit(user, &amount);
+    }
+
+    fn setup_fresh() -> (Env, XLMWrapperClient<'static>, StellarAssetClient<'static>, Address) {
         let env = Env::default();
         env.mock_all_auths();
         let admin = Address::generate(&env);
+        let sac_contract = env.register_stellar_asset_contract_v2(admin.clone());
+        let native_asset = sac_contract.address();
+        let sac = StellarAssetClient::new(&env, &native_asset);
         let contract_id = env.register_contract(None, XLMWrapper);
         let client = XLMWrapperClient::new(&env, &contract_id);
         let token = Address::generate(&env);
@@ -651,11 +841,11 @@ mod invariants {
             &token,
             &String::from_str(&env, "Wrapped XLM"),
             &String::from_str(&env, "wXLM"),
+            &native_asset,
         );
-        (env, client, admin)
+        (env, client, sac, admin)
     }
 
-    /// Helper to verify the supply conservation invariant
     fn verify_supply_conservation(env: &Env, client: &XLMWrapperClient<'_>, users: &[Address]) {
         let total_supply = client.total_supply();
         let balance_sum: i128 = users.iter().map(|u| client.balance_of(u)).sum();
@@ -666,458 +856,338 @@ mod invariants {
         );
     }
 
-    // =========================================================================
-    // INVARIANT 1: Conservation of Supply
-    // =========================================================================
-    /// After any operation, the sum of all user balances must equal total_supply.
-    /// This is the fundamental invariant of any token contract.
     #[test]
     fn invariant_supply_conservation_after_deposit() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let user1 = Address::generate(&env);
         let user2 = Address::generate(&env);
         let user3 = Address::generate(&env);
-
-        // Deposit to multiple users
-        client.deposit(&user1, &1000);
+        fund_and_deposit(&env, &sac, &client, &user1, 1000);
         verify_supply_conservation(&env, &client, &[user1.clone(), user2.clone(), user3.clone()]);
-
-        client.deposit(&user2, &500);
+        fund_and_deposit(&env, &sac, &client, &user2, 500);
         verify_supply_conservation(&env, &client, &[user1.clone(), user2.clone(), user3.clone()]);
-
-        client.deposit(&user3, &250);
+        fund_and_deposit(&env, &sac, &client, &user3, 250);
         verify_supply_conservation(&env, &client, &[user1, user2, user3]);
     }
 
     #[test]
     fn invariant_supply_conservation_after_transfer() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let alice = Address::generate(&env);
         let bob = Address::generate(&env);
         let carol = Address::generate(&env);
-
-        client.deposit(&alice, &1000);
+        fund_and_deposit(&env, &sac, &client, &alice, 1000);
         let supply_before = client.total_supply();
-
-        // Multiple transfers
         client.transfer(&alice, &bob, &300);
         verify_supply_conservation(&env, &client, &[alice.clone(), bob.clone(), carol.clone()]);
-
         client.transfer(&bob, &carol, &150);
         verify_supply_conservation(&env, &client, &[alice.clone(), bob.clone(), carol.clone()]);
-
         client.transfer(&alice, &carol, &100);
         verify_supply_conservation(&env, &client, &[alice, bob, carol]);
-
         let supply_after = client.total_supply();
-        assert_eq!(
-            supply_before, supply_after,
-            "INVARIANT VIOLATION: Supply changed during transfers"
-        );
+        assert_eq!(supply_before, supply_after, "INVARIANT VIOLATION: Supply changed during transfers");
     }
 
     #[test]
     fn invariant_supply_conservation_after_withdraw() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let user = Address::generate(&env);
-
-        client.deposit(&user, &1000);
+        fund_and_deposit(&env, &sac, &client, &user, 1000);
         let supply_before_withdraw = client.total_supply();
-
         client.withdraw(&user, &300);
         verify_supply_conservation(&env, &client, &[user.clone()]);
-
-        // Invariant: supply decreases by exactly the withdrawn amount
-        assert_eq!(
-            client.total_supply(),
-            supply_before_withdraw - 300,
-            "INVARIANT VIOLATION: Supply not reduced correctly after withdraw"
-        );
-
+        assert_eq!(client.total_supply(), supply_before_withdraw - 300, "INVARIANT VIOLATION: Supply not reduced correctly after withdraw");
         verify_supply_conservation(&env, &client, &[user]);
     }
 
     #[test]
     fn invariant_supply_conservation_after_burn() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let user = Address::generate(&env);
-
-        client.deposit(&user, &1000);
+        fund_and_deposit(&env, &sac, &client, &user, 1000);
         let supply_before_burn = client.total_supply();
-
         client.burn(&user, &300);
         verify_supply_conservation(&env, &client, &[user.clone()]);
-
-        assert_eq!(
-            client.total_supply(),
-            supply_before_burn - 300,
-            "INVARIANT VIOLATION: Supply not reduced correctly after burn"
-        );
-
+        assert_eq!(client.total_supply(), supply_before_burn - 300, "INVARIANT VIOLATION: Supply not reduced correctly after burn");
         verify_supply_conservation(&env, &client, &[user]);
     }
 
-    // =========================================================================
-    // INVARIANT 2: 1:1 Peg Maintenance
-    // =========================================================================
-    /// The total supply of wXLM should always equal the total amount of
-    /// native XLM held by the contract (minus any burned tokens).
     #[test]
     fn invariant_one_to_one_peg_after_operations() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let user = Address::generate(&env);
-
-        // Deposit creates 1:1 peg
-        client.deposit(&user, &1000);
-        assert_eq!(
-            client.total_supply(),
-            client.balance_of(&user),
-            "INVARIANT VIOLATION: 1:1 peg broken after deposit"
-        );
-
-        // Transfer maintains peg
+        fund_and_deposit(&env, &sac, &client, &user, 1000);
+        assert_eq!(client.total_supply(), client.balance_of(&user), "INVARIANT VIOLATION: 1:1 peg broken after deposit");
         let bob = Address::generate(&env);
         client.transfer(&user, &bob, &300);
-        assert_eq!(
-            client.total_supply(),
-            client.balance_of(&user) + client.balance_of(&bob),
-            "INVARIANT VIOLATION: 1:1 peg broken after transfer"
-        );
-
-        // Withdraw maintains peg
+        assert_eq!(client.total_supply(), client.balance_of(&user) + client.balance_of(&bob), "INVARIANT VIOLATION: 1:1 peg broken after transfer");
         client.withdraw(&user, &200);
-        assert_eq!(
-            client.total_supply(),
-            client.balance_of(&user) + client.balance_of(&bob),
-            "INVARIANT VIOLATION: 1:1 peg broken after withdraw"
-        );
+        assert_eq!(client.total_supply(), client.balance_of(&user) + client.balance_of(&bob), "INVARIANT VIOLATION: 1:1 peg broken after withdraw");
     }
 
-    // =========================================================================
-    // INVARIANT 3: Non-Negative Balances
-    // =========================================================================
-    /// All balances must always be non-negative (>= 0).
     #[test]
     fn invariant_non_negative_balances() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let user = Address::generate(&env);
-
-        assert!(
-            client.balance_of(&user) >= 0,
-            "INVARIANT VIOLATION: Initial balance is negative"
-        );
-
-        client.deposit(&user, &100);
-        assert!(
-            client.balance_of(&user) >= 0,
-            "INVARIANT VIOLATION: Balance negative after deposit"
-        );
-
+        assert!(client.balance_of(&user) >= 0, "INVARIANT VIOLATION: Initial balance is negative");
+        fund_and_deposit(&env, &sac, &client, &user, 100);
+        assert!(client.balance_of(&user) >= 0, "INVARIANT VIOLATION: Balance negative after deposit");
         client.withdraw(&user, &100);
-        assert!(
-            client.balance_of(&user) >= 0,
-            "INVARIANT VIOLATION: Balance negative after withdraw"
-        );
+        assert!(client.balance_of(&user) >= 0, "INVARIANT VIOLATION: Balance negative after withdraw");
     }
 
-    // =========================================================================
-    // INVARIANT 4: Conservation of Value in Transfer
-    // =========================================================================
-    /// In any transfer, the sum of sender and receiver balances before
-    /// must equal the sum after the transfer.
     #[test]
     fn invariant_transfer_value_conservation() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let alice = Address::generate(&env);
         let bob = Address::generate(&env);
-
-        client.deposit(&alice, &1000);
-
+        fund_and_deposit(&env, &sac, &client, &alice, 1000);
         let alice_before = client.balance_of(&alice);
         let bob_before = client.balance_of(&bob);
         let sum_before = alice_before + bob_before;
-
         client.transfer(&alice, &bob, &400);
-
         let alice_after = client.balance_of(&alice);
         let bob_after = client.balance_of(&bob);
         let sum_after = alice_after + bob_after;
-
-        assert_eq!(
-            sum_before, sum_after,
-            "INVARIANT VIOLATION: Value not conserved in transfer"
-        );
-
-        assert_eq!(
-            alice_before - alice_after,
-            400,
-            "INVARIANT VIOLATION: Sender balance not reduced correctly"
-        );
-
-        assert_eq!(
-            bob_after - bob_before,
-            400,
-            "INVARIANT VIOLATION: Receiver balance not increased correctly"
-        );
+        assert_eq!(sum_before, sum_after, "INVARIANT VIOLATION: Value not conserved in transfer");
+        assert_eq!(alice_before - alice_after, 400, "INVARIANT VIOLATION: Sender balance not reduced correctly");
+        assert_eq!(bob_after - bob_before, 400, "INVARIANT VIOLATION: Receiver balance not increased correctly");
     }
 
-    // =========================================================================
-    // INVARIANT 5: Allowance Accounting
-    // =========================================================================
-    /// After transfer_from, the allowance must decrease by exactly the
-    /// transferred amount.
     #[test]
     fn invariant_allowance_decrease_on_transfer_from() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let owner = Address::generate(&env);
         let spender = Address::generate(&env);
         let recipient = Address::generate(&env);
-
-        client.deposit(&owner, &1000);
+        fund_and_deposit(&env, &sac, &client, &owner, 1000);
         client.approve(&owner, &spender, &500);
-
         let allowance_before = client.allowance(&owner, &spender);
-
         client.transfer_from(&spender, &owner, &recipient, &200);
-
         let allowance_after = client.allowance(&owner, &spender);
-
-        assert_eq!(
-            allowance_before - allowance_after,
-            200,
-            "INVARIANT VIOLATION: Allowance not reduced correctly"
-        );
+        assert_eq!(allowance_before - allowance_after, 200, "INVARIANT VIOLATION: Allowance not reduced correctly");
     }
 
     #[test]
     #[should_panic]
     fn invariant_allowance_cannot_exceed_approval() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let owner = Address::generate(&env);
         let spender = Address::generate(&env);
         let recipient = Address::generate(&env);
-
-        client.deposit(&owner, &1000);
+        fund_and_deposit(&env, &sac, &client, &owner, 1000);
         client.approve(&owner, &spender, &100);
-
-        // Attempting to spend more than approved should fail
         client.transfer_from(&spender, &owner, &recipient, &150);
     }
 
-    // =========================================================================
-    // INVARIANT 6: No Double Spend
-    // =========================================================================
-    /// A user cannot spend the same tokens twice (either directly or via approval).
+    #[test]
+    fn invariant_decrease_allowance_reduces_correctly() {
+        let (env, client, sac, _) = setup_fresh();
+        let owner = Address::generate(&env);
+        let spender = Address::generate(&env);
+        fund_and_deposit(&env, &sac, &client, &owner, 1000);
+        client.approve(&owner, &spender, &500);
+        let before = client.allowance(&owner, &spender);
+        client.decrease_allowance(&owner, &spender, &200);
+        let after = client.allowance(&owner, &spender);
+        assert_eq!(before - after, 200, "INVARIANT VIOLATION: decrease_allowance did not reduce allowance by the correct amount");
+    }
+
+    #[test]
+    fn invariant_decrease_allowance_to_zero_resets_cleanly() {
+        let (env, client, sac, _) = setup_fresh();
+        let owner = Address::generate(&env);
+        let spender = Address::generate(&env);
+        fund_and_deposit(&env, &sac, &client, &owner, 1000);
+        client.approve(&owner, &spender, &300);
+        client.decrease_allowance(&owner, &spender, &300);
+        assert_eq!(client.allowance(&owner, &spender), 0, "INVARIANT VIOLATION: Allowance not zero after full decrease");
+    }
+
+    #[test]
+    fn invariant_decrease_allowance_preserves_supply() {
+        let (env, client, sac, _) = setup_fresh();
+        let owner = Address::generate(&env);
+        let spender = Address::generate(&env);
+        fund_and_deposit(&env, &sac, &client, &owner, 1000);
+        client.approve(&owner, &spender, &500);
+        let supply_before = client.total_supply();
+        client.decrease_allowance(&owner, &spender, &100);
+        assert_eq!(client.total_supply(), supply_before, "INVARIANT VIOLATION: decrease_allowance changed total supply");
+    }
+
+    #[test]
+    fn invariant_decrease_allowance_does_not_affect_balances() {
+        let (env, client, sac, _) = setup_fresh();
+        let owner = Address::generate(&env);
+        let spender = Address::generate(&env);
+        fund_and_deposit(&env, &sac, &client, &owner, 1000);
+        client.approve(&owner, &spender, &500);
+        let owner_bal_before = client.balance_of(&owner);
+        let spender_bal_before = client.balance_of(&spender);
+        client.decrease_allowance(&owner, &spender, &100);
+        assert_eq!(client.balance_of(&owner), owner_bal_before, "INVARIANT VIOLATION: decrease_allowance changed owner balance");
+        assert_eq!(client.balance_of(&spender), spender_bal_before, "INVARIANT VIOLATION: decrease_allowance changed spender balance");
+    }
+
+    #[test]
+    fn invariant_increase_allowance_preserves_invariants() {
+        let (env, client, sac, _) = setup_fresh();
+        let owner = Address::generate(&env);
+        let spender = Address::generate(&env);
+        let users = [owner.clone(), spender.clone()];
+        fund_and_deposit(&env, &sac, &client, &owner, 1000);
+        client.approve(&owner, &spender, &500);
+        let supply_before = client.total_supply();
+        let owner_bal_before = client.balance_of(&owner);
+        let spender_bal_before = client.balance_of(&spender);
+        client.increase_allowance(&owner, &spender, &200);
+        assert_eq!(client.total_supply(), supply_before);
+        assert_eq!(client.balance_of(&owner), owner_bal_before);
+        assert_eq!(client.balance_of(&spender), spender_bal_before);
+        verify_supply_conservation(&env, &client, &users);
+    }
+
+    #[test]
+    fn invariant_allowance_decrease_and_transfer_from_sequence() {
+        let (env, client, sac, _) = setup_fresh();
+        let owner = Address::generate(&env);
+        let spender = Address::generate(&env);
+        let recipient = Address::generate(&env);
+        let users = [owner.clone(), spender.clone(), recipient.clone()];
+        fund_and_deposit(&env, &sac, &client, &owner, 1000);
+        client.approve(&owner, &spender, &500);
+        client.decrease_allowance(&owner, &spender, &200);
+        assert_eq!(client.allowance(&owner, &spender), 300);
+        client.transfer_from(&spender, &owner, &recipient, &300);
+        assert_eq!(client.allowance(&owner, &spender), 0);
+        assert_eq!(client.balance_of(&recipient), 300);
+        verify_supply_conservation(&env, &client, &users);
+    }
+
     #[test]
     #[should_panic]
     fn invariant_no_double_spend_direct() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let alice = Address::generate(&env);
         let bob = Address::generate(&env);
         let carol = Address::generate(&env);
-
-        client.deposit(&alice, &100);
-
-        // First transfer succeeds
+        fund_and_deposit(&env, &sac, &client, &alice, 100);
         client.transfer(&alice, &bob, &60);
-
-        // Alice now has 40, trying to spend 60 more should fail
         client.transfer(&alice, &carol, &60);
     }
 
-    // =========================================================================
-    // INVARIANT 7: Total Supply Monotonicity
-    // =========================================================================
-    /// Total supply only increases via deposit and only decreases via withdraw/burn.
-    /// Transfers and approvals do not affect total supply.
     #[test]
     fn invariant_supply_only_changes_via_deposit_withdraw_burn() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let alice = Address::generate(&env);
         let bob = Address::generate(&env);
-
         let initial_supply = client.total_supply();
         assert_eq!(initial_supply, 0);
-
-        // Deposit increases supply
-        client.deposit(&alice, &500);
+        fund_and_deposit(&env, &sac, &client, &alice, 500);
         assert_eq!(client.total_supply(), 500);
         verify_supply_conservation(&env, &client, &[alice.clone(), bob.clone()]);
-
-        // Transfer does not change supply
         client.transfer(&alice, &bob, &200);
-        assert_eq!(
-            client.total_supply(),
-            500,
-            "INVARIANT VIOLATION: Transfer changed total supply"
-        );
+        assert_eq!(client.total_supply(), 500, "INVARIANT VIOLATION: Transfer changed total supply");
         verify_supply_conservation(&env, &client, &[alice.clone(), bob.clone()]);
-
-        // Approve does not change supply
         client.approve(&alice, &bob, &100);
-        assert_eq!(
-            client.total_supply(),
-            500,
-            "INVARIANT VIOLATION: Approve changed total supply"
-        );
+        assert_eq!(client.total_supply(), 500, "INVARIANT VIOLATION: Approve changed total supply");
         verify_supply_conservation(&env, &client, &[alice.clone(), bob.clone()]);
-
-        // Burn decreases supply
         client.burn(&alice, &100);
         assert_eq!(client.total_supply(), 400);
         verify_supply_conservation(&env, &client, &[alice, bob]);
     }
 
-    // =========================================================================
-    // INVARIANT 8: Zero Amount Handling
-    // =========================================================================
-    /// The contract should handle zero amounts appropriately.
     #[test]
     #[should_panic]
     fn invariant_deposit_zero_rejected() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let user = Address::generate(&env);
-
         client.deposit(&user, &0);
     }
 
     #[test]
     #[should_panic]
     fn invariant_withdraw_zero_rejected() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let user = Address::generate(&env);
-
-        client.deposit(&user, &100);
+        fund_and_deposit(&env, &sac, &client, &user, 100);
         client.withdraw(&user, &0);
     }
 
     #[test]
     #[should_panic]
     fn invariant_burn_zero_rejected() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let user = Address::generate(&env);
-
-        client.deposit(&user, &100);
+        fund_and_deposit(&env, &sac, &client, &user, 100);
         client.burn(&user, &0);
     }
 
-    // =========================================================================
-    // INVARIANT 9: Idempotency Properties
-    // =========================================================================
-    /// Certain operations should have predictable idempotent-like behavior.
     #[test]
     fn invariant_approve_overwrites() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let owner = Address::generate(&env);
         let spender = Address::generate(&env);
-
-        client.deposit(&owner, &1000);
+        fund_and_deposit(&env, &sac, &client, &owner, 1000);
         client.approve(&owner, &spender, &100);
         assert_eq!(client.allowance(&owner, &spender), 100);
-
-        // New approval should overwrite, not add
         client.approve(&owner, &spender, &200);
-        assert_eq!(
-            client.allowance(&owner, &spender),
-            200,
-            "INVARIANT VIOLATION: Approve did not overwrite previous allowance"
-        );
+        assert_eq!(client.allowance(&owner, &spender), 200, "INVARIANT VIOLATION: Approve did not overwrite previous allowance");
     }
 
-    // =========================================================================
-    // PROPERTY-BASED INVARIANT TESTS
-    // =========================================================================
-    /// These tests verify invariants across sequences of operations.
-
     #[test]
     fn property_sequence_invariant() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let alice = Address::generate(&env);
         let bob = Address::generate(&env);
         let carol = Address::generate(&env);
-
-        // Sequence of operations that should maintain invariants
-        client.deposit(&alice, &1000);
+        fund_and_deposit(&env, &sac, &client, &alice, 1000);
         verify_supply_conservation(&env, &client, &[alice.clone(), bob.clone(), carol.clone()]);
-
-        client.deposit(&bob, &500);
+        fund_and_deposit(&env, &sac, &client, &bob, 500);
         verify_supply_conservation(&env, &client, &[alice.clone(), bob.clone(), carol.clone()]);
-
         client.transfer(&alice, &bob, &200);
         verify_supply_conservation(&env, &client, &[alice.clone(), bob.clone(), carol.clone()]);
-
         client.approve(&bob, &carol, &300);
         verify_supply_conservation(&env, &client, &[alice.clone(), bob.clone(), carol.clone()]);
-
         client.transfer_from(&carol, &bob, &alice, &150);
         verify_supply_conservation(&env, &client, &[alice.clone(), bob.clone(), carol.clone()]);
-
         client.withdraw(&alice, &100);
         verify_supply_conservation(&env, &client, &[alice.clone(), bob.clone(), carol.clone()]);
 
         // Verify final invariants
         let total_balance = client.balance_of(&alice) + client.balance_of(&bob) + client.balance_of(&carol);
-
-        assert_eq!(
-            client.total_supply(),
-            total_balance,
-            "PROPERTY VIOLATION: Supply invariant broken after operation sequence"
-        );
-
-        assert!(
-            client.balance_of(&alice) >= 0 && client.balance_of(&bob) >= 0 && client.balance_of(&carol) >= 0,
-            "PROPERTY VIOLATION: Negative balance detected"
-        );
+        assert_eq!(client.total_supply(), total_balance, "PROPERTY VIOLATION: Supply invariant broken after operation sequence");
+        assert!(client.balance_of(&alice) >= 0 && client.balance_of(&bob) >= 0 && client.balance_of(&carol) >= 0, "PROPERTY VIOLATION: Negative balance detected");
     }
 
     #[test]
     fn property_deposit_withdraw_symmetry() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let user = Address::generate(&env);
-
-        // Deposit then withdraw same amount should return to initial state
         let initial_supply = client.total_supply();
         let initial_balance = client.balance_of(&user);
-
-        client.deposit(&user, &500);
+        fund_and_deposit(&env, &sac, &client, &user, 500);
         verify_supply_conservation(&env, &client, &[user.clone()]);
-
         client.withdraw(&user, &500);
         verify_supply_conservation(&env, &client, &[user.clone()]);
-
-        assert_eq!(
-            client.total_supply(),
-            initial_supply,
-            "PROPERTY VIOLATION: Deposit-withdraw symmetry broken for supply"
-        );
-
-        assert_eq!(
-            client.balance_of(&user),
-            initial_balance,
-            "PROPERTY VIOLATION: Deposit-withdraw symmetry broken for balance"
-        );
+        assert_eq!(client.total_supply(), initial_supply, "PROPERTY VIOLATION: Deposit-withdraw symmetry broken for supply");
+        assert_eq!(client.balance_of(&user), initial_balance, "PROPERTY VIOLATION: Deposit-withdraw symmetry broken for balance");
     }
 
     #[test]
     fn property_transfer_reversibility_check() {
-        let (env, client, _) = setup_fresh();
+        let (env, client, sac, _) = setup_fresh();
         let alice = Address::generate(&env);
         let bob = Address::generate(&env);
-
-        client.deposit(&alice, &1000);
+        fund_and_deposit(&env, &sac, &client, &alice, 1000);
         verify_supply_conservation(&env, &client, &[alice.clone(), bob.clone()]);
-
         let alice_initial = client.balance_of(&alice);
         let bob_initial = client.balance_of(&bob);
-
-        // Transfer A -> B
         client.transfer(&alice, &bob, &300);
         verify_supply_conservation(&env, &client, &[alice.clone(), bob.clone()]);
-
-        // Transfer B -> A (reverse)
         client.transfer(&bob, &alice, &300);
         verify_supply_conservation(&env, &client, &[alice.clone(), bob.clone()]);
-
         // After round-trip, balances should be back to original
         assert_eq!(
             client.balance_of(&alice),
@@ -1134,36 +1204,24 @@ mod invariants {
 
     #[test]
     fn property_multi_user_supply_conservation() {
-        let (env, client, _) = setup_fresh();
-        let users: std::vec::Vec<Address> = (0..10).map(|_| Address::generate(&env)).collect();
-
-        // Random-like deposits
+        let (env, client, sac, _) = setup_fresh();
+        let mut users = std::vec::Vec::new();
         let mut total_deposited = 0_i128;
-        for (i, user) in users.iter().enumerate() {
+        for i in 0..10 {
+            let user = Address::generate(&env);
             let amount = ((i + 1) * 100) as i128;
-            client.deposit(user, &amount);
+            fund_and_deposit(&env, &sac, &client, &user, amount);
             total_deposited += amount;
+            users.push(user);
             verify_supply_conservation(&env, &client, &users);
         }
-
-        assert_eq!(
-            client.total_supply(),
-            total_deposited,
-            "PROPERTY VIOLATION: Total supply doesn't match total deposited"
-        );
-
-        // Random-like transfers between users
+        assert_eq!(client.total_supply(), total_deposited, "PROPERTY VIOLATION: Total supply doesn't match total deposited");
         for i in 0..5 {
-            let from = users.get(i).unwrap();
-            let to = users.get(i + 1).unwrap();
+            let from = &users[i];
+            let to = &users[i + 1];
             client.transfer(from, to, &50);
             verify_supply_conservation(&env, &client, &users);
         }
-
-        assert_eq!(
-            client.total_supply(),
-            total_deposited,
-            "PROPERTY VIOLATION: Supply changed during transfers"
-        );
+        assert_eq!(client.total_supply(), total_deposited, "PROPERTY VIOLATION: Supply changed during transfers");
     }
 }