feat(vault): add Kani harnesses for transfer correctness + fix compile errors (#490)

[ZuLu0890]

Summary

Closes #490 — Add Kani harness for vault.transfer correctness under adversarial input.

---

Compilation fixes

The vault contract had several bugs preventing compilation:

• StorageKey::MetaKey → StorageKey::Meta — 5 occurrences replaced; MetaKey variant does not exist in the enum.
• Missing get_max_deduct() method — referenced by deduct and batch_deduct but never defined; added as a public view function.
• Dead code warning — added #[allow(dead_code)] to the orphaned migrate() helper.

Correctness fixes

• deduct() did not check pause state — deposit and batch_deduct both called require_not_paused(); deduct did not, allowing deductions through the circuit-breaker. Fixed.
• Deposit event topic count — EVENT_SCHEMA.md specifies topic[0] = Symbol("deposit"), topic[1] = caller Address. The implementation only emitted 1 topic. Fixed to match schema.

Test fixes

• deduct_while_paused_succeeds → deduct_while_paused_fails (#[should_panic])
• batch_deduct_while_paused_succeeds → batch_deduct_while_paused_fails (#[should_panic])
• Deposit event tests updated to assert 2 topics + verify caller address
• Fuzz tests: removed duplicate else branch that caused parse error
• settlement/test.rs: fixed _third_party → third_party in setup_contract()
• Fixed unused variable warnings (settlement, step_cap)

Kani formal verification (issue #490)

Added contracts/vault/src/kani_proofs.rs with 7 adversarial harnesses:

Harness	Property verified
kani_deduct_balance_non_negative	balance ≥ 0 after any valid deduction
kani_deduct_strictly_reduces_balance	deduct always strictly decreases balance
kani_deposit_no_overflow	checked_add succeeds for all in-range deposits
kani_deposit_overflow_detected	checked_add returns None on overflow (panic path sound)
kani_max_deduct_enforced	amount > max_deduct is rejected before any mutation
kani_batch_deduct_total_no_overflow	batch total accumulation stays non-negative and correct
kani_withdraw_balance_non_negative	withdraw mirrors deduct invariant under adversarial amounts

All harnesses use symbolic inputs via kani::any() + kani::assume() to cover the full input space, including adversarial edge cases (e.g. near i128::MAX, zero boundaries).

The file is guarded with #[cfg(kani)] — normal cargo test / CI runs skip it entirely. Vault Cargo.toml declares cfg(kani) as a known check-cfg to suppress the rustc unexpected_cfgs warning.

Running harnesses locally

cargo install --locked kani-verifier
cargo kani --package callora-vault

CI verification

Check	Result
cargo fmt --check	✅
cargo clippy -D warnings	✅
cargo test --workspace	✅ 270 tests (179 vault + 52 settlement + 39 revenue-pool)

[drips-wave]

@ZuLu0890 Great news! 🎉 Based on an automated assessment of this PR, the linked Wave issue(s) no longer count against your application limits.

You can now already apply to more issues while waiting for a review of this PR. Keep up the great work! 🚀

Learn more about application limits