out_entry.lamports.set_sol_value(    out_entry        .lamports        .sol_value()                                // stale stored value        .checked_sub(*quote.qtys.sol_value().out()) // derived from fresh out_sol_val        .ok_or(SanctumSolsProgErr(SanctumSolsErr::Math))?,);

out_entry.lamports.set_sol_value(    out_sol_val        .checked_sub(*quote.qtys.sol_value().out())        .ok_or(SanctumSolsProgErr(SanctumSolsErr::Math))?,);

let is_self_swap = inp_out.out().holding_ata() == inp_out.inp().holding_ata();process_deposit_holding(abr, cpi, out, ctl_pre, *inp_out.out(), chq, is_self_swap)

let is_relinquish_holding = pre.out() == holding.ata();...if !is_relinquish_holding {    hold_lamports.set_sol_value(hold.sol_value().checked_sub(*qtys.sol_value().out())?);}

if !is_self_swap {    lamports.set_sol_value(lamports.sol_value().checked_add(*holding.sol_value())?);}lamports.set_outstanding(lamports.outstanding().checked_add(*qtys.out())?);...process_mint(abr, cpi, &out, *qtys.out(), out_pool_bump)

#[inline]pub const fn apply(&self, amount: u64) -> Option<u64> {    if self.0.is_zero() {        return Some(0);    }    let Ratio { n, d } = self.0;    let d = d as u128;    let n = n as u128;    let x = amount as u128;    // unchecked-arith: mul will not overflow because    // both x and n are <= u64::MAX    let xn = x * n;    // unchecked-arith: ratio is not 0 so d != 0    let res = xn.div_ceil(d);    u128_to_u64_checked(res)}

let mint = mint_of(holding_accs.mint())?;if mint.freeze_auth().is_some() {    return Err(SanctumSolsProgErr(SanctumSolsErr::InitMintHasFreezeAuth).into());}

pub const TWTM_IX_IS_SIGNER: TWTMIxAccFlags = TWTMIxAccFlags {    pre: TWTM_IX_PRE_IS_SIGNER,    suf: TWTM_IX_SUF_IS_SIGNER,    progs: TOKEN_SYS_PROG_IS_WRITER,  // <-- wrong constant};

use crate::instructions::common::{TokenSysProgs, TOKEN_SYS_PROG_IS_SIGNER, TOKEN_SYS_PROG_IS_WRITER};
pub const TWTM_IX_IS_SIGNER: TWTMIxAccFlags = TWTMIxAccFlags {    pre: TWTM_IX_PRE_IS_SIGNER,    suf: TWTM_IX_SUF_IS_SIGNER,    progs: TOKEN_SYS_PROG_IS_SIGNER,  // fixed};

/// is_pool_solvent <=> dep_due_checked returns Some#[kani::proof]fn is_pool_solvent_iff_dep_due_checked_some() {    let x = pool();    kani::assume(is_pool_solvent(x));    assert!(x.0.dep_due_checked(x.1).is_some());
    let y = pool();    kani::assume(y.0.dep_due_checked(y.1).is_some());    assert!(is_pool_solvent(y));}
/// dep_due = liq_avail + outstanding - protocol_fee#[kani::proof]fn dep_due_formula_correct() {    let (p, pool_acc_lamports) = solvent_pool();    let dep_due = p.dep_due_checked(pool_acc_lamports).unwrap();    let liq_avail = p.liq_avail_checked(pool_acc_lamports).unwrap();    assert_eq!(dep_due, liq_avail + p.outstanding() - p.protocol_fee());}
/// depositing N lamports increases dep_due by exactly N#[kani::proof]fn dep_due_increases_with_deposits() {    let (p, pool_acc_lamports) = solvent_pool();    let deposit: u64 = kani::any();    // ... overflow guards ...    assert_eq!(dep_due_after, dep_due_before + deposit);}
/// increasing outstanding by N increases dep_due by exactly N#[kani::proof]fn dep_due_increases_with_outstanding() {    let (p, pool_acc_lamports) = solvent_pool();    let outstanding_inc: u64 = kani::any();    // ... overflow guards ...    assert_eq!(dep_due_after, dep_due_before + outstanding_inc);}
/// increasing protocol_fee by N decreases dep_due by exactly N#[kani::proof]fn dep_due_decreases_with_protocol_fee() {    let (p, pool_acc_lamports) = solvent_pool();    let fee_inc: u64 = kani::any();    // ... overflow guards ...    assert_eq!(dep_due_after + fee_inc, dep_due_before);}
/// claiming <= surplus preserves dep_due >= mint_supply#[kani::proof]fn claim_preserves_solvency() {    let (p, pool_acc_lamports) = solvent_pool();    let mint_supply: u64 = kani::any();    kani::assume(mint_supply <= dep_due);    kani::assume(claim_amt <= surplus);    kani::assume(claim_amt <= liq_avail);    // ...    assert_eq!(new_dep_due, dep_due - claim_amt);    assert!(new_dep_due >= mint_supply);}
/// rebalancing SOL out (lamports ↓, outstanding ↑) preserves dep_due#[kani::proof]fn rebal_sol_out_preserves_dep_due() {    let (p, pool_acc_lamports) = solvent_pool();    let rebal_amt: u64 = kani::any();    kani::assume(rebal_amt <= liq_avail);    // new_pool_acc_lamports = pool_acc_lamports - rebal_amt    // new_outstanding = outstanding + rebal_amt    assert_eq!(dep_due_after, dep_due_before);}
/// rebalancing SOL in (lamports ↑, outstanding ↓) preserves dep_due#[kani::proof]fn rebal_sol_inp_preserves_dep_due() {    let (p, pool_acc_lamports) = solvent_pool();    let rebal_amt: u64 = kani::any();    kani::assume(rebal_amt <= outstanding);    // new_pool_acc_lamports = pool_acc_lamports + rebal_amt    // new_outstanding = outstanding - rebal_amt    assert_eq!(dep_due_after, dep_due_before);}

/// surplus preserved: outstanding_dec = claim_lamports - protocol_fee_lamports#[kani::proof]fn claim_holding_preserves_surplus() {    let (claim_lamports, args) = valid_claim_holding_args();    let result = quote_claim_holding(claim_lamports, &args);        if let Ok(quote) = result {        let protocol_fee_lamports = quote.protocol_fees.total();        let expected_outstanding_dec = (claim_lamports as i128) - (protocol_fee_lamports as i128);        assert_eq!(quote.outstanding_dec, expected_outstanding_dec);    }}
/// protocol fees relationship: outstanding_dec = claim_lamports - protocol_fees#[kani::proof]fn claim_holding_protocol_fees_bounded() {    let (claim_lamports, args) = valid_claim_holding_args();    let result = quote_claim_holding(claim_lamports, &args);        if let Ok(quote) = result {        let protocol_fee_lamports = quote.protocol_fees.total();        let expected = (claim_lamports as i128) - (protocol_fee_lamports as i128);        assert_eq!(quote.outstanding_dec, expected);    }}
/// output tokens bounded by holding balance#[kani::proof]#[kani::unwind(2)]fn claim_holding_output_bounded() {    let (claim_lamports, args) = valid_claim_holding_args();    let result = quote_claim_holding(claim_lamports, &args);        if let Ok(quote) = result {        assert!(*quote.qtys.amt().out() <= args.holding_balance);    }}
/// input amounts correctly preserved#[kani::proof]#[kani::unwind(2)]fn claim_holding_input_preserved() {    let (claim_lamports, args) = valid_claim_holding_args();    let result = quote_claim_holding(claim_lamports, &args);        if let Ok(quote) = result {        assert_eq!(*quote.qtys.amt().inp(), claim_lamports);        assert_eq!(*quote.qtys.sol_value().inp(), claim_lamports);    }}

depositor_due = pool.lamports - rent_exempt_lamports - protocol_fee_lamports + outstanding_lamports

/// Prove: deposit_fee + out == sol_value.out from claim (AftFee invariant)./// This ensures no lamports are created or destroyed by the fee split.#[kani::proof]#[kani::unwind(2)]fn swap_holding_fee_decomposition() {    let claim_inp: u64 = kani::any();    let claim_out: u64 = kani::any();    let sol_value_inp: u64 = kani::any();    let sol_value_out: u64 = kani::any();    let outstanding_dec: i128 = kani::any();    let pf_fixed: u64 = kani::any();    let pf_perf: u64 = kani::any();    let deposit_fee_nanos: u32 = kani::any();
    kani::assume(claim_inp > 0 && claim_inp <= 10);    kani::assume(claim_out <= 10);    kani::assume(sol_value_inp > 0 && sol_value_inp <= 10);    kani::assume(sol_value_out > 0 && sol_value_out <= 10);    kani::assume(outstanding_dec >= -10 && outstanding_dec <= 10);    kani::assume(pf_fixed <= 10);    kani::assume(pf_perf <= 10);    kani::assume(deposit_fee_nanos <= 1_000_000_000);
    let chq = ClaimHoldingQuote {        qtys: RebalInpOut::const_from_destr(RebalQtysDestr {            amt: InpOut::const_from_destr(InpOutDestr {                inp: claim_inp,                out: claim_out,            }),            sol_value: InpOut::const_from_destr(InpOutDestr {                inp: sol_value_inp,                out: sol_value_out,            }),        }),        outstanding_dec,        protocol_fees: ProtocolV1FeeLamports::const_from_destr(ProtocolV1FeesDestr {            fixed: pf_fixed,            perf: pf_perf,        }),    };
    let deposit_fee = Nanos::new(deposit_fee_nanos).unwrap();
    // Pool state for RRArgs    let rent_exempt: u64 = kani::any();    let pool_outstanding: u64 = kani::any();    let pool_pf: u64 = kani::any();    let pool_acc: u64 = kani::any();    let rrr_nanos: u32 = kani::any();
    kani::assume(rent_exempt <= pool_acc);    kani::assume(pool_acc <= 100);    kani::assume(pool_outstanding <= 100);    kani::assume(pool_pf <= 100);    kani::assume(rrr_nanos <= 1_000_000_000);
    let rr = RRArgs {        rrr_limit: Nanos::new(rrr_nanos).unwrap(),        pool_lamports: PoolV1LamportVals::const_from_destr(PoolV1LamportsDestr {            rent_exempt,            outstanding: pool_outstanding,            protocol_fee: pool_pf,        }),        pool_acc_lamports: pool_acc,    };
    let result = swap_holding_quote_from_claim(&chq, deposit_fee, &rr);
    if let Ok(q) = result {        assert_eq!(            q.deposit_fee_lamports + *q.qtys.out(),            sol_value_out,            "fee + out must equal sol_value.out"        );    }}
/// Prove: output amount (after deposit fee) is bounded by the claim's sol_value.out./// Ensures deposit fee is always non-negative.#[kani::proof]#[kani::unwind(2)]fn swap_holding_out_bounded_by_sol_value() {    let sol_value_out: u64 = kani::any();    let deposit_fee_nanos: u32 = kani::any();
    kani::assume(sol_value_out > 0 && sol_value_out <= 10);    kani::assume(deposit_fee_nanos <= 1_000_000_000);
    let chq = ClaimHoldingQuote {        qtys: RebalInpOut::const_from_destr(RebalQtysDestr {            amt: InpOut::const_from_destr(InpOutDestr { inp: 5, out: 5 }),            sol_value: InpOut::const_from_destr(InpOutDestr {                inp: 5,                out: sol_value_out,            }),        }),        outstanding_dec: 5,        protocol_fees: ProtocolV1FeeLamports::const_from_destr(ProtocolV1FeesDestr {            fixed: 0,            perf: 0,        }),    };
    let deposit_fee = Nanos::new(deposit_fee_nanos).unwrap();
    let rr = RRArgs {        rrr_limit: Nanos::new(0).unwrap(),        pool_lamports: PoolV1LamportVals::const_from_destr(PoolV1LamportsDestr {            rent_exempt: 10,            outstanding: 0,            protocol_fee: 0,        }),        pool_acc_lamports: 50,    };
    let result = swap_holding_quote_from_claim(&chq, deposit_fee, &rr);
    if let Ok(q) = result {        assert!(            *q.qtys.out() <= sol_value_out,            "out must not exceed sol_value.out (deposit fee >= 0)"        );    }}
/// Prove: the input token amount is preserved from the claim quote.#[kani::proof]#[kani::unwind(2)]fn swap_holding_input_preserved() {    let claim_inp: u64 = kani::any();    let sol_value_out: u64 = kani::any();    let deposit_fee_nanos: u32 = kani::any();
    kani::assume(claim_inp > 0 && claim_inp <= 10);    kani::assume(sol_value_out > 0 && sol_value_out <= 10);    kani::assume(deposit_fee_nanos <= 1_000_000_000);
    let chq = ClaimHoldingQuote {        qtys: RebalInpOut::const_from_destr(RebalQtysDestr {            amt: InpOut::const_from_destr(InpOutDestr {                inp: claim_inp,                out: 5,            }),            sol_value: InpOut::const_from_destr(InpOutDestr {                inp: claim_inp,                out: sol_value_out,            }),        }),        outstanding_dec: 5,        protocol_fees: ProtocolV1FeeLamports::const_from_destr(ProtocolV1FeesDestr {            fixed: 0,            perf: 0,        }),    };
    let deposit_fee = Nanos::new(deposit_fee_nanos).unwrap();
    let rr = RRArgs {        rrr_limit: Nanos::new(0).unwrap(),        pool_lamports: PoolV1LamportVals::const_from_destr(PoolV1LamportsDestr {            rent_exempt: 10,            outstanding: 0,            protocol_fee: 0,        }),        pool_acc_lamports: 50,    };
    let result = swap_holding_quote_from_claim(&chq, deposit_fee, &rr);
    if let Ok(q) = result {        assert_eq!(            *q.qtys.inp(),            claim_inp,            "input amount must be preserved from claim"        );    }}
/// Prove: holding sol_value and amt are preserved from the claim quote.#[kani::proof]#[kani::unwind(2)]fn swap_holding_holding_fields_preserved() {    let claim_out: u64 = kani::any();    let sol_value_out: u64 = kani::any();    let deposit_fee_nanos: u32 = kani::any();
    kani::assume(claim_out > 0 && claim_out <= 10);    kani::assume(sol_value_out > 0 && sol_value_out <= 10);    kani::assume(deposit_fee_nanos <= 1_000_000_000);
    let chq = ClaimHoldingQuote {        qtys: RebalInpOut::const_from_destr(RebalQtysDestr {            amt: InpOut::const_from_destr(InpOutDestr {                inp: 5,                out: claim_out,            }),            sol_value: InpOut::const_from_destr(InpOutDestr {                inp: 5,                out: sol_value_out,            }),        }),        outstanding_dec: 5,        protocol_fees: ProtocolV1FeeLamports::const_from_destr(ProtocolV1FeesDestr {            fixed: 0,            perf: 0,        }),    };
    let deposit_fee = Nanos::new(deposit_fee_nanos).unwrap();
    let rr = RRArgs {        rrr_limit: Nanos::new(0).unwrap(),        pool_lamports: PoolV1LamportVals::const_from_destr(PoolV1LamportsDestr {            rent_exempt: 10,            outstanding: 0,            protocol_fee: 0,        }),        pool_acc_lamports: 50,    };
    let result = swap_holding_quote_from_claim(&chq, deposit_fee, &rr);
    if let Ok(q) = result {        assert_eq!(            *q.holding.amt(),            claim_out,            "holding.amt must be claim's amt.out"        );        assert_eq!(            *q.holding.sol_value(),            sol_value_out,            "holding.sol_value must be claim's sol_value.out"        );    }}
/// End-to-end swap_other: run quote_claim_holding → swap_holding_quote_from_claim,/// then verify both inp and out pool surplus is preserved.#[kani::proof]#[kani::unwind(2)]fn swap_other_end_to_end_surplus() {    use crate::accounts::{        PoolLiqLamportVals, PoolLiqLamportsDestr,        ProtocolV1FeeRatios,    };    use crate::typedefs::HoldingV1LamportVals;    use crate::typedefs::HoldingV1LamportsDestr;    use crate::utils::protocol_fee_ratio;
    // --- Inp pool holding state ---    let outstanding: u64 = kani::any();    let sol_value: u64 = kani::any();    let holding_balance: u64 = kani::any();    let claim_lamports: u64 = kani::any();
    kani::assume(outstanding > 0 && outstanding <= 10);    kani::assume(sol_value > 0 && sol_value <= 10);    kani::assume(holding_balance > 0 && holding_balance <= 10);    kani::assume(claim_lamports > 0 && claim_lamports <= outstanding);
    let holding = HoldingV1LamportVals::const_from_destr(HoldingV1LamportsDestr {        outstanding,        sol_value,    });    let pool_liq = PoolLiqLamportVals::const_from_destr(PoolLiqLamportsDestr {        total: 5,        rent_exempt: 5, // liq_avail = 0    });    let protocol_fees = ProtocolV1FeeRatios::const_from_destr(ProtocolV1FeesDestr {        fixed: protocol_fee_ratio(Nanos::new(0).unwrap()),        perf: protocol_fee_ratio(Nanos::new(0).unwrap()),    });
    let inp_args = QuoteClaimHoldingArgs {        holding,        holding_balance,        protocol_fees,        pool: pool_liq,    };
    // Step 1: claim_holding    let chq = match quote_claim_holding(claim_lamports, &inp_args) {        Ok(x) => x,        Err(_) => return,    };
    // --- Out pool state ---    let out_rent: u64 = kani::any();    let out_outstanding: u64 = kani::any();    let out_pf: u64 = kani::any();    let out_acc: u64 = kani::any();    let out_mint_supply: u64 = kani::any();    let deposit_fee_nanos: u32 = kani::any();
    kani::assume(out_rent > 0 && out_rent <= 10);    kani::assume(out_acc >= out_rent && out_acc <= 10);    kani::assume(out_outstanding <= 10);    kani::assume(out_pf <= 10);    kani::assume(deposit_fee_nanos <= 1_000_000_000);
    let out_pool = PoolV1LamportVals::const_from_destr(PoolV1LamportsDestr {        rent_exempt: out_rent,        outstanding: out_outstanding,        protocol_fee: out_pf,    });
    // Out pool must be solvent before    let out_dep_due_before = match out_pool.dep_due_checked(out_acc) {        Some(x) => x,        None => return,    };    kani::assume(out_mint_supply <= out_dep_due_before);
    let deposit_fee = Nanos::new(deposit_fee_nanos).unwrap();    let rr = RRArgs {        rrr_limit: Nanos::new(0).unwrap(), // no reserve ratio floor        pool_lamports: out_pool,        pool_acc_lamports: out_acc,    };
    // Step 2: swap_holding_quote_from_claim    let shq = match swap_holding_quote_from_claim(&chq, deposit_fee, &rr) {        Ok(x) => x,        Err(_) => return,    };
    let delta = *shq.qtys.out(); // amount minted to user = outstanding increment
    // --- Verify out pool surplus preserved ---    if let Some(new_outstanding) = out_outstanding.checked_add(delta) {        let new_out_pool = PoolV1LamportVals::const_from_destr(PoolV1LamportsDestr {            rent_exempt: out_rent,            outstanding: new_outstanding,            protocol_fee: out_pf,        });        if let Some(new_dep_due) = new_out_pool.dep_due_checked(out_acc) {            let new_mint_supply = match out_mint_supply.checked_add(delta) {                Some(x) => x,                None => return,            };            // Surplus is exactly preserved            assert_eq!(                new_dep_due.saturating_sub(new_mint_supply),                out_dep_due_before.saturating_sub(out_mint_supply),                "out pool surplus must be preserved after swap_other"            );        }    }
    // --- Verify inp pool surplus preserved ---    // claim_holding: outstanding_dec = claim_lamports - pf_total (with zero fees, outstanding_dec = claim_lamports)    // dep_due_change = -claim_lamports, mint_supply_change = -claim_lamports    // surplus_change = 0    let pf_total = match chq.protocol_fees.total_checked() {        Some(x) => x,        None => return,    };    let expected_outstanding_dec = (claim_lamports as i128) - (pf_total as i128);    assert_eq!(        chq.outstanding_dec,        expected_outstanding_dec,        "inp pool: outstanding_dec must equal claim_lamports - pf_total"    );}

// ============================================================// SOL Out proofs// ============================================================
/// Prove: outstanding always equals out AND sol_value.out == out./// Tests on the full outer function (includes verify_rebal_above_ceil).#[kani::proof]#[kani::unwind(2)]fn sol_out_outstanding_equals_out() {    let out: u64 = kani::any();    let sol_out_loss_tol_raw: u32 = kani::any();    let rent_exempt: u64 = kani::any();    let outstanding: u64 = kani::any();    let protocol_fee: u64 = kani::any();    let pool_acc_lamports: u64 = kani::any();    let rrr_ceil_raw: u32 = kani::any();
    kani::assume(out > 0 && out <= 10_000_000);    kani::assume(rent_exempt <= pool_acc_lamports);    kani::assume(pool_acc_lamports <= 10_000_000);    kani::assume(outstanding <= 10_000_000);    kani::assume(protocol_fee <= 10_000_000);    kani::assume(sol_out_loss_tol_raw <= 10_000_000);    kani::assume(rrr_ceil_raw <= 1_000_000_000);
    let sol_out_loss_tol = Nanos::new(sol_out_loss_tol_raw).unwrap();    let rrr_limit = Nanos::new(rrr_ceil_raw).unwrap();    let pool_lamports = PoolV1LamportVals::const_from_destr(PoolV1LamportsDestr {        rent_exempt,        outstanding,        protocol_fee,    });    let rr = RRArgs {        rrr_limit,        pool_lamports,        pool_acc_lamports,    };
    let result = quote_rebal_sol_out_exact_out_sol_val(out, sol_out_loss_tol, &rr);    if let Ok(q) = result {        assert_eq!(q.outstanding, out);        assert_eq!(*q.sol_value.out(), out);    }}
/// Prove: inp_sol_val <= out (loss tolerance means pool accepts less LST value)./// Tests the inner function directly for tractability.#[kani::proof]#[kani::unwind(2)]fn sol_out_inp_bounded_by_out() {    let out: u64 = kani::any();    let pool_total: u64 = kani::any();    let pool_rent_exempt: u64 = kani::any();    let sol_out_loss_tol_raw: u32 = kani::any();
    kani::assume(out > 0 && out <= 10_000_000);    kani::assume(pool_rent_exempt <= pool_total);    kani::assume(pool_total <= 10_000_000);    kani::assume(sol_out_loss_tol_raw <= 10_000_000);
    let pool = PoolLiqLamportVals::const_from_destr(PoolLiqLamportsDestr {        total: pool_total,        rent_exempt: pool_rent_exempt,    });    let sol_out_loss_tol = Nanos::new(sol_out_loss_tol_raw).unwrap();
    let result = quote_rebal_sol_out_exact_out_sol_val_inner(out, &pool, sol_out_loss_tol);    if let Ok(q) = result {        assert!(            *q.sol_value.inp() <= *q.sol_value.out(),            "inp sol value must not exceed out sol value"        );    }}
/// Prove: dep_due is preserved after a sol_out rebalance./// pool_acc_lamports -= out, pool.outstanding += out => dep_due unchanged.#[kani::proof]#[kani::unwind(2)]fn sol_out_preserves_dep_due() {    let out: u64 = kani::any();    let pool_total: u64 = kani::any();    let pool_rent_exempt: u64 = kani::any();    let sol_out_loss_tol_raw: u32 = kani::any();    let pool_outstanding: u64 = kani::any();    let pool_protocol_fee: u64 = kani::any();
    kani::assume(out > 0 && out <= 10_000_000);    kani::assume(pool_rent_exempt <= pool_total);    kani::assume(pool_total <= 10_000_000);    kani::assume(pool_outstanding <= 10_000_000);    kani::assume(pool_protocol_fee <= 10_000_000);    kani::assume(sol_out_loss_tol_raw <= 10_000_000);
    let pool = PoolLiqLamportVals::const_from_destr(PoolLiqLamportsDestr {        total: pool_total,        rent_exempt: pool_rent_exempt,    });    let sol_out_loss_tol = Nanos::new(sol_out_loss_tol_raw).unwrap();
    let result = quote_rebal_sol_out_exact_out_sol_val_inner(out, &pool, sol_out_loss_tol);    if let Ok(q) = result {        let pool_lamports = PoolV1LamportVals::const_from_destr(PoolV1LamportsDestr {            rent_exempt: pool_rent_exempt,            outstanding: pool_outstanding,            protocol_fee: pool_protocol_fee,        });        let dep_due = match pool_lamports.dep_due_checked(pool_total) {            Some(x) => x,            None => return,        };
        let new_pool_acc = match pool_total.checked_sub(*q.sol_value.out()) {            Some(x) => x,            None => return,        };        let new_outstanding = match pool_outstanding.checked_add(q.outstanding) {            Some(x) => x,            None => return,        };        let new_pool_lamports = PoolV1LamportVals::const_from_destr(PoolV1LamportsDestr {            rent_exempt: pool_rent_exempt,            outstanding: new_outstanding,            protocol_fee: pool_protocol_fee,        });        let new_dep_due = match new_pool_lamports.dep_due_checked(new_pool_acc) {            Some(x) => x,            None => return,        };
        assert_eq!(new_dep_due, dep_due, "dep_due must be preserved");    }}
// ============================================================// SOL Inp proofs// ============================================================
/// Prove: inp == outstanding (lamports_returning) + protocol_fees./// This is critical: the SOL entering the pool must exactly equal/// the outstanding being settled plus the protocol's cut.#[kani::proof]#[kani::unwind(2)]fn sol_inp_inp_is_returning_plus_fees() {    let out: u64 = kani::any();    let outstanding: u64 = kani::any();    let sol_value: u64 = kani::any();    let holding_balance: u64 = kani::any();    let fixed_fee_nanos: u32 = kani::any();    let perf_fee_nanos: u32 = kani::any();
    kani::assume(out > 0 && out <= 10_000_000);    kani::assume(holding_balance > 0 && holding_balance <= 10_000_000);    kani::assume(out <= holding_balance);    kani::assume(outstanding > 0 && outstanding <= 10_000_000);    kani::assume(sol_value > 0 && sol_value <= 10_000_000);    kani::assume(fixed_fee_nanos < 1_000_000_000);    kani::assume(perf_fee_nanos < 1_000_000_000);
    let holding = HoldingV1LamportVals::const_from_destr(HoldingV1LamportsDestr {        outstanding,        sol_value,    });    let pf = ProtocolV1FeeRatios::const_from_destr(ProtocolV1FeesDestr {        fixed: protocol_fee_ratio(Nanos::new(fixed_fee_nanos).unwrap()),        perf: protocol_fee_ratio(Nanos::new(perf_fee_nanos).unwrap()),    });
    let result = quote_rebal_sol_inp_exact_out_inner(out, &holding, holding_balance, &pf);
    if let Ok(q) = result {        let total_pf = q.protocol_fees.total_checked().unwrap();        assert_eq!(            *q.qtys.amt().inp(),            q.outstanding + total_pf,            "inp must equal lamports_returning + protocol_fees"        );    }}
/// Prove: lamports_returning (outstanding) is bounded by holding.outstanding./// Since out <= holding_balance, ceil(out/holding_balance * outstanding) <= outstanding.#[kani::proof]#[kani::unwind(2)]fn sol_inp_outstanding_bounded() {    let out: u64 = kani::any();    let outstanding: u64 = kani::any();    let sol_value: u64 = kani::any();    let holding_balance: u64 = kani::any();    let fixed_fee_nanos: u32 = kani::any();    let perf_fee_nanos: u32 = kani::any();
    kani::assume(out > 0 && out <= 10);    kani::assume(holding_balance > 0 && holding_balance <= 10);    kani::assume(out <= holding_balance);    kani::assume(outstanding > 0 && outstanding <= 10);    kani::assume(sol_value > 0 && sol_value <= 10);    kani::assume(fixed_fee_nanos < 1_000_000_000);    kani::assume(perf_fee_nanos < 1_000_000_000);
    let holding = HoldingV1LamportVals::const_from_destr(HoldingV1LamportsDestr {        outstanding,        sol_value,    });    let pf = ProtocolV1FeeRatios::const_from_destr(ProtocolV1FeesDestr {        fixed: protocol_fee_ratio(Nanos::new(fixed_fee_nanos).unwrap()),        perf: protocol_fee_ratio(Nanos::new(perf_fee_nanos).unwrap()),    });
    let result = quote_rebal_sol_inp_exact_out_inner(out, &holding, holding_balance, &pf);
    if let Ok(q) = result {        assert!(            q.outstanding <= outstanding,            "lamports_returning must not exceed holding outstanding"        );    }}
/// Prove: dep_due is preserved after sol_inp rebalance./// pool_acc_lamports += inp, pool.outstanding -= returning, pool.protocol_fee += pf/// => dep_due unchanged.#[kani::proof]#[kani::unwind(2)]fn sol_inp_preserves_dep_due() {    let out: u64 = kani::any();    let h_outstanding: u64 = kani::any();    let h_sol_value: u64 = kani::any();    let holding_balance: u64 = kani::any();    let fixed_fee_nanos: u32 = kani::any();    let perf_fee_nanos: u32 = kani::any();
    kani::assume(out > 0 && out <= 10);    kani::assume(holding_balance > 0 && holding_balance <= 10);    kani::assume(out <= holding_balance);    kani::assume(h_outstanding > 0 && h_outstanding <= 10);    kani::assume(h_sol_value > 0 && h_sol_value <= 10);    kani::assume(fixed_fee_nanos < 1_000_000_000);    kani::assume(perf_fee_nanos < 1_000_000_000);
    let holding = HoldingV1LamportVals::const_from_destr(HoldingV1LamportsDestr {        outstanding: h_outstanding,        sol_value: h_sol_value,    });    let pf_ratios = ProtocolV1FeeRatios::const_from_destr(ProtocolV1FeesDestr {        fixed: protocol_fee_ratio(Nanos::new(fixed_fee_nanos).unwrap()),        perf: protocol_fee_ratio(Nanos::new(perf_fee_nanos).unwrap()),    });
    let rent_exempt: u64 = kani::any();    let pool_outstanding: u64 = kani::any();    let pool_pf: u64 = kani::any();    let pool_acc: u64 = kani::any();
    kani::assume(rent_exempt <= pool_acc);    kani::assume(pool_acc <= 100);    kani::assume(pool_outstanding <= 100);    kani::assume(pool_pf <= 100);
    let pool_lamports = PoolV1LamportVals::const_from_destr(PoolV1LamportsDestr {        rent_exempt,        outstanding: pool_outstanding,        protocol_fee: pool_pf,    });    let dep_due = match pool_lamports.dep_due_checked(pool_acc) {        Some(x) => x,        None => return,    };
    let result =        quote_rebal_sol_inp_exact_out_inner(out, &holding, holding_balance, &pf_ratios);    if let Ok(q) = result {        let total_pf = match q.protocol_fees.total_checked() {            Some(x) => x,            None => return,        };
        let new_pool_acc = match pool_acc.checked_add(*q.qtys.amt().inp()) {            Some(x) => x,            None => return,        };        let new_outstanding = match pool_outstanding.checked_sub(q.outstanding) {            Some(x) => x,            None => return,        };        let new_pf = match pool_pf.checked_add(total_pf) {            Some(x) => x,            None => return,        };
        let new_pool_lamports = PoolV1LamportVals::const_from_destr(PoolV1LamportsDestr {            rent_exempt,            outstanding: new_outstanding,            protocol_fee: new_pf,        });        let new_dep_due = match new_pool_lamports.dep_due_checked(new_pool_acc) {            Some(x) => x,            None => return,        };
        assert_eq!(new_dep_due, dep_due, "dep_due must be preserved");    }}
/// Prove: when sol_value <= outstanding (no gains / depreciation),/// performance fee must be 0. Only fixed fee should apply.#[kani::proof]#[kani::unwind(2)]fn sol_inp_no_perf_fee_when_no_gains() {    let out: u64 = kani::any();    let outstanding: u64 = kani::any();    let sol_value: u64 = kani::any();    let holding_balance: u64 = kani::any();    let fixed_fee_nanos: u32 = kani::any();    let perf_fee_nanos: u32 = kani::any();
    kani::assume(out > 0 && out <= 10_000_000);    kani::assume(holding_balance > 0 && holding_balance <= 10_000_000);    kani::assume(out <= holding_balance);    kani::assume(outstanding > 0 && outstanding <= 10_000_000);    kani::assume(sol_value > 0 && sol_value <= 10_000_000);    kani::assume(sol_value <= outstanding);    kani::assume(fixed_fee_nanos < 1_000_000_000);    kani::assume(perf_fee_nanos < 1_000_000_000);
    let holding = HoldingV1LamportVals::const_from_destr(HoldingV1LamportsDestr {        outstanding,        sol_value,    });    let pf = ProtocolV1FeeRatios::const_from_destr(ProtocolV1FeesDestr {        fixed: protocol_fee_ratio(Nanos::new(fixed_fee_nanos).unwrap()),        perf: protocol_fee_ratio(Nanos::new(perf_fee_nanos).unwrap()),    });
    let result = quote_rebal_sol_inp_exact_out_inner(out, &holding, holding_balance, &pf);
    if let Ok(q) = result {        assert_eq!(            *q.protocol_fees.perf(),            0,            "perf fee must be 0 when sol_value <= outstanding"        );    }}
/// Prove: sol_value.inp equals amt.inp (for SOL input, both are the same).#[kani::proof]#[kani::unwind(2)]fn sol_inp_sol_value_inp_equals_amt_inp() {    let out: u64 = kani::any();    let outstanding: u64 = kani::any();    let sol_value: u64 = kani::any();    let holding_balance: u64 = kani::any();    let fixed_fee_nanos: u32 = kani::any();    let perf_fee_nanos: u32 = kani::any();
    kani::assume(out > 0 && out <= 10_000_000);    kani::assume(holding_balance > 0 && holding_balance <= 10_000_000);    kani::assume(out <= holding_balance);    kani::assume(outstanding > 0 && outstanding <= 10_000_000);    kani::assume(sol_value > 0 && sol_value <= 10_000_000);    kani::assume(fixed_fee_nanos < 1_000_000_000);    kani::assume(perf_fee_nanos < 1_000_000_000);
    let holding = HoldingV1LamportVals::const_from_destr(HoldingV1LamportsDestr {        outstanding,        sol_value,    });    let pf = ProtocolV1FeeRatios::const_from_destr(ProtocolV1FeesDestr {        fixed: protocol_fee_ratio(Nanos::new(fixed_fee_nanos).unwrap()),        perf: protocol_fee_ratio(Nanos::new(perf_fee_nanos).unwrap()),    });
    let result = quote_rebal_sol_inp_exact_out_inner(out, &holding, holding_balance, &pf);
    if let Ok(q) = result {        assert_eq!(            *q.qtys.sol_value().inp(),            *q.qtys.amt().inp(),            "sol_value.inp must equal amt.inp for SOL input"        );    }}