1#![no_std]
2
3extern crate alloc;
4#[cfg(any(test, feature = "std", feature = "schemars", feature = "borsh-schema"))]
5extern crate std;
6
7pub mod abort;
8pub mod actions;
9pub mod address_book;
10pub mod effects;
11pub mod error;
12pub mod fee;
13pub mod math;
14pub mod restrictions;
15pub mod state;
16
17#[doc(hidden)]
18pub mod test_utils;
19pub mod transitions;
20pub mod types;
21pub mod utils;
22
23pub const ACTION_RECOVERY_ENABLED: bool = cfg!(feature = "action-recovery");
25pub const ACTION_SYNC_EXTERNAL_ENABLED: bool = cfg!(feature = "action-sync-external");
27pub const ACTION_REFRESH_FEES_ENABLED: bool = cfg!(feature = "action-refresh-fees");
29pub const ACTION_ALLOCATION_LIFECYCLE_ENABLED: bool = cfg!(feature = "action-allocation-lifecycle");
31pub const ACTION_REFRESH_LIFECYCLE_ENABLED: bool = cfg!(feature = "action-refresh-lifecycle");
33pub const ACTION_PAUSE_ENABLED: bool = cfg!(feature = "action-pause");
35
36pub use actions::{
37 apply_action, convert_to_assets, convert_to_assets_bounded, convert_to_assets_ceil,
38 convert_to_assets_ceil_bounded, convert_to_shares, convert_to_shares_bounded,
39 convert_to_shares_ceil, convert_to_shares_ceil_bounded, effective_totals, plan_idle_payout,
40 preview_deposit_shares, preview_withdraw_assets, EffectiveTotals, IdlePayoutPlan, KernelAction,
41 KernelResult, PayoutOutcome,
42};
43pub use address_book::AddressBook;
44pub use fee::{Fee, FeeSlot, Fees, FeesSpec};
45pub use math::number::Number;
46pub use math::wad::{
47 compute_fee_shares, compute_fee_shares_from_assets, compute_management_fee_shares,
48 mul_div_ceil, mul_div_floor, mul_wad_floor, total_assets_for_fee_accrual, Wad, MAX_FEE_WAD,
49 MAX_MANAGEMENT_FEE_WAD, MAX_PERFORMANCE_FEE_WAD, YEAR_NS,
50};
51pub use restrictions::{RestrictionKind, RestrictionMode, Restrictions};
52pub use state::escrow::{
53 apply_settlement, can_apply_settlement, compute_escrow_stats, find_by_owner, is_stale,
54 settle_proportional, settle_proportional_raw, total_burn, total_refund, EscrowEntry,
55 EscrowSettlement, EscrowStats, SettlementResult,
56};
57pub use state::op_state::{
58 AllocatingState, AllocationPlanEntry, IdleState, OpState, PayoutState, RefreshingState,
59 TargetId, WithdrawingState,
60};
61pub use state::queue::{
62 can_enqueue, can_partially_satisfy, can_satisfy_withdrawal, compute_full_withdrawal,
63 compute_idle_settlement, compute_partial_withdrawal, compute_queue_status, compute_settlement,
64 compute_settlement_by_price, count_satisfiable, find_request_status, is_past_cooldown,
65 is_valid_withdrawal_amount, PendingWithdrawal, QueueError, QueueStatus, WithdrawQueue,
66 WithdrawalRequestStatus, WithdrawalResult, DEFAULT_COOLDOWN_NS, MAX_PENDING, MAX_QUEUE_LENGTH,
67 MIN_WITHDRAWAL_ASSETS,
68};
69pub use state::vault::{FeeAccrualAnchor, VaultConfig, VaultState};
70pub use transitions::{
71 allocation_step_callback, complete_allocation, complete_refresh, payout_complete,
72 refresh_step_callback, start_allocation, start_refresh, start_withdrawal, stop_withdrawal,
73 withdrawal_collected, withdrawal_settled, withdrawal_step_callback, TransitionError,
74 TransitionRes, TransitionResult, WithdrawalRequest,
75};
76
77#[cfg(kani)]
78mod kani_proofs {
79 use alloc::{vec, vec::Vec};
80
81 use super::*;
82 #[cfg(feature = "action-recovery")]
83 use crate::actions::plan_emergency_reset;
84 use crate::actions::{
85 apply_payout_settlement, apply_withdrawal_request_plan, pending_withdrawal_head,
86 plan_payout_settlement, validate_queue_head, withdrawal_request_from_head,
87 WithdrawalRequestPlan,
88 };
89 use crate::effects::KernelEffect;
90
91 const MAX_AMOUNT: u128 = 32;
92 const OWNER: Address = Address([0x11; 32]);
93 const RECEIVER: Address = Address([0x22; 32]);
94 const SELF: Address = Address([0x33; 32]);
95 const SECOND_OWNER: Address = Address([0x44; 32]);
96 const SECOND_RECEIVER: Address = Address([0x55; 32]);
97
98 fn bounded_amount() -> u128 {
99 let amount = kani::any::<u128>();
100 kani::assume(amount <= MAX_AMOUNT);
101 amount
102 }
103
104 fn nonzero_bounded_amount() -> u128 {
105 let amount = bounded_amount();
106 kani::assume(amount > 0);
107 amount
108 }
109
110 fn zero_fee_config() -> VaultConfig {
111 VaultConfig {
112 fees: FeesSpec::zero(),
113 min_withdrawal_assets: 0,
114 withdrawal_cooldown_ns: 0,
115 max_pending_withdrawals: 3,
116 paused: false,
117 virtual_shares: 0,
118 virtual_assets: 0,
119 }
120 }
121
122 #[cfg(feature = "action-refresh-fees")]
123 fn active_fee_config() -> VaultConfig {
124 VaultConfig {
125 fees: FeesSpec::new(
126 FeeSlot::new(Wad::one() / 10, Address([0x66; 32])),
127 FeeSlot::zero(),
128 None,
129 ),
130 min_withdrawal_assets: 0,
131 withdrawal_cooldown_ns: 0,
132 max_pending_withdrawals: 3,
133 paused: false,
134 virtual_shares: 0,
135 virtual_assets: 0,
136 }
137 }
138
139 fn assert_accounting_invariant(state: &VaultState) {
140 assert!(state.check_invariant());
141 assert_eq!(
142 state.total_assets,
143 state.idle_assets + state.external_assets
144 );
145 }
146
147 fn assert_asset_sum(state: &VaultState) {
148 assert_eq!(
149 state.total_assets,
150 state.idle_assets + state.external_assets
151 );
152 }
153
154 fn assert_address_eq(left: Address, right: Address) {
155 assert_eq!(left.0[0], right.0[0]);
156 assert_eq!(left.0[1], right.0[1]);
157 assert_eq!(left.0[2], right.0[2]);
158 assert_eq!(left.0[3], right.0[3]);
159 assert_eq!(left.0[4], right.0[4]);
160 assert_eq!(left.0[5], right.0[5]);
161 assert_eq!(left.0[6], right.0[6]);
162 assert_eq!(left.0[7], right.0[7]);
163 assert_eq!(left.0[8], right.0[8]);
164 assert_eq!(left.0[9], right.0[9]);
165 assert_eq!(left.0[10], right.0[10]);
166 assert_eq!(left.0[11], right.0[11]);
167 assert_eq!(left.0[12], right.0[12]);
168 assert_eq!(left.0[13], right.0[13]);
169 assert_eq!(left.0[14], right.0[14]);
170 assert_eq!(left.0[15], right.0[15]);
171 assert_eq!(left.0[16], right.0[16]);
172 assert_eq!(left.0[17], right.0[17]);
173 assert_eq!(left.0[18], right.0[18]);
174 assert_eq!(left.0[19], right.0[19]);
175 assert_eq!(left.0[20], right.0[20]);
176 assert_eq!(left.0[21], right.0[21]);
177 assert_eq!(left.0[22], right.0[22]);
178 assert_eq!(left.0[23], right.0[23]);
179 assert_eq!(left.0[24], right.0[24]);
180 assert_eq!(left.0[25], right.0[25]);
181 assert_eq!(left.0[26], right.0[26]);
182 assert_eq!(left.0[27], right.0[27]);
183 assert_eq!(left.0[28], right.0[28]);
184 assert_eq!(left.0[29], right.0[29]);
185 assert_eq!(left.0[30], right.0[30]);
186 assert_eq!(left.0[31], right.0[31]);
187 }
188
189 fn bounded_state() -> VaultState {
190 let idle = bounded_amount();
191 let external = bounded_amount();
192 let shares = bounded_amount();
193 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO)
194 }
195
196 fn allocation_plan(first: u128, second: u128) -> Vec<AllocationPlanEntry> {
197 vec![
198 AllocationPlanEntry::new(0, first),
199 AllocationPlanEntry::new(1, second),
200 ]
201 }
202
203 fn enqueue_withdrawal(
204 state: &mut VaultState,
205 owner: Address,
206 receiver: Address,
207 shares: u128,
208 expected_assets: u128,
209 requested_at_ns: TimestampNs,
210 ) -> u64 {
211 state
212 .withdraw_queue
213 .enqueue(owner, receiver, shares, expected_assets, requested_at_ns, 3)
214 .unwrap()
215 }
216
217 fn assert_transfer_shares_effect(
218 effect: &KernelEffect,
219 expected_from: Address,
220 expected_to: Address,
221 expected_shares: u128,
222 ) {
223 match effect {
224 KernelEffect::TransferShares { from, to, shares } => {
225 assert_address_eq(*from, expected_from);
226 assert_address_eq(*to, expected_to);
227 assert_eq!(*shares, expected_shares);
228 }
229 _ => panic!("expected transfer shares effect"),
230 }
231 }
232
233 fn assert_emit_event_effect(effect: &KernelEffect) {
234 match effect {
235 KernelEffect::EmitEvent { .. } => {}
236 _ => panic!("expected emit event effect"),
237 }
238 }
239
240 #[cfg(feature = "action-refresh-fees")]
241 fn assert_mint_shares_effect(effect: &KernelEffect) -> u128 {
242 match effect {
243 KernelEffect::MintShares { shares, .. } => {
244 assert!(*shares > 0);
245 *shares
246 }
247 _ => panic!("refresh fees must not move assets or non-fee shares"),
248 }
249 }
250
251 fn assert_refund_owner_is_owner(refund_owner: Option<Address>) {
252 match refund_owner {
253 Some(owner) => assert_address_eq(owner, OWNER),
254 None => panic!("expected refund owner"),
255 }
256 }
257
258 #[kani::proof]
259 fn bounded_initial_state_preserves_total_asset_invariant() {
260 let idle = bounded_amount();
261 let external = bounded_amount();
262 let shares = bounded_amount();
263
264 let state =
265 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
266
267 assert!(state.check_invariant());
268 assert_eq!(
269 state.total_assets,
270 state.idle_assets + state.external_assets
271 );
272 assert_eq!(state.total_shares, shares);
273 assert_eq!(state.withdraw_queue.status().length, 0);
274 }
275
276 #[kani::proof]
277 fn restore_to_idle_preserves_total_asset_invariant() {
278 let idle = bounded_amount();
279 let external = bounded_amount();
280 let restored = bounded_amount();
281 let shares = bounded_amount();
282
283 let mut state =
284 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
285 state.restore_to_idle(restored);
286
287 assert!(state.check_invariant());
288 assert_eq!(state.idle_assets, idle + restored);
289 assert_eq!(state.external_assets, external);
290 assert_eq!(state.total_assets, idle + external + restored);
291 }
292
293 #[kani::proof]
294 fn withdrawal_queue_enqueue_preserves_cached_escrow_and_claimability() {
295 let shares = nonzero_bounded_amount();
296 let expected_assets = bounded_amount();
297 let mut queue = WithdrawQueue::new();
298
299 let id = queue
300 .enqueue(
301 OWNER,
302 RECEIVER,
303 shares,
304 expected_assets,
305 TimestampNs::ZERO,
306 3,
307 )
308 .unwrap();
309
310 let status = queue.status();
311 assert_eq!(id, 0);
312 assert!(queue.check_invariants_with_max(3));
313 assert_eq!(status.length, 1);
314 assert_eq!(status.total_escrow_shares, shares);
315 assert_eq!(status.total_expected_assets, expected_assets);
316 assert!(queue.contains(id));
317 assert!(queue.head().is_some());
318 }
319
320 #[kani::proof]
321 #[kani::unwind(8)]
322 fn two_entry_withdrawal_queue_preserves_cached_escrow_and_claimability() {
323 let first_shares = nonzero_bounded_amount();
324 let second_shares = nonzero_bounded_amount();
325 let first_expected_assets = bounded_amount();
326 let second_expected_assets = bounded_amount();
327 let mut queue = WithdrawQueue::new();
328
329 let first_id = queue
330 .enqueue(
331 OWNER,
332 RECEIVER,
333 first_shares,
334 first_expected_assets,
335 TimestampNs::ZERO,
336 3,
337 )
338 .unwrap();
339 let second_id = queue
340 .enqueue(
341 RECEIVER,
342 OWNER,
343 second_shares,
344 second_expected_assets,
345 TimestampNs::ZERO,
346 3,
347 )
348 .unwrap();
349
350 let status = queue.status();
351 let first = queue
352 .get(first_id)
353 .expect("first withdrawal should be queued");
354 let second = queue
355 .get(second_id)
356 .expect("second withdrawal should be queued");
357
358 assert_eq!(first_id, 0);
359 assert_eq!(second_id, 1);
360 assert!(queue.check_invariants_with_max(3));
361 assert_eq!(status.length, 2);
362 assert_eq!(status.total_escrow_shares, first_shares + second_shares);
363 assert_eq!(
364 status.total_expected_assets,
365 first_expected_assets + second_expected_assets
366 );
367 assert!(queue.contains(first_id));
368 assert!(queue.contains(second_id));
369 assert_eq!(queue.head().map(|(id, _)| id), Some(first_id));
370 assert_eq!(first.escrow_shares, first_shares);
371 assert_eq!(first.expected_assets, first_expected_assets);
372 assert_eq!(second.escrow_shares, second_shares);
373 assert_eq!(second.expected_assets, second_expected_assets);
374 }
375
376 #[kani::proof]
377 #[kani::unwind(8)]
378 fn two_entry_withdrawal_queue_dequeues_fifo_and_preserves_cache() {
379 let first_shares = nonzero_bounded_amount();
380 let second_shares = nonzero_bounded_amount();
381 let first_expected_assets = bounded_amount();
382 let second_expected_assets = bounded_amount();
383 let mut queue = WithdrawQueue::new();
384
385 let first_id = queue
386 .enqueue(
387 OWNER,
388 RECEIVER,
389 first_shares,
390 first_expected_assets,
391 TimestampNs::ZERO,
392 3,
393 )
394 .unwrap();
395 let second_id = queue
396 .enqueue(
397 RECEIVER,
398 OWNER,
399 second_shares,
400 second_expected_assets,
401 TimestampNs::ZERO,
402 3,
403 )
404 .unwrap();
405
406 let (dequeued_id, dequeued) = queue.dequeue().expect("first withdrawal should dequeue");
407 let status = queue.status();
408
409 assert_eq!(dequeued_id, first_id);
410 assert_eq!(dequeued.escrow_shares, first_shares);
411 assert_eq!(dequeued.expected_assets, first_expected_assets);
412 assert!(queue.check_invariants_with_max(3));
413 assert_eq!(status.length, 1);
414 assert_eq!(status.total_escrow_shares, second_shares);
415 assert_eq!(status.total_expected_assets, second_expected_assets);
416 assert!(!queue.contains(first_id));
417 assert!(queue.contains(second_id));
418 assert_eq!(queue.head().map(|(id, _)| id), Some(second_id));
419 }
420
421 #[kani::proof]
422 #[kani::unwind(40)]
423 fn withdrawal_request_plan_preserves_accounting_and_enqueues_exact_escrow() {
424 let idle = bounded_amount();
425 let external = bounded_amount();
426 let total_shares = nonzero_bounded_amount();
427 let shares = nonzero_bounded_amount();
428 let expected_assets = bounded_amount();
429 kani::assume(idle + external <= MAX_AMOUNT);
430 let config = zero_fee_config();
431 let state = VaultState::with_initial(
432 idle + external,
433 total_shares,
434 idle,
435 external,
436 TimestampNs::ZERO,
437 );
438 let before = state.clone();
439 let plan = WithdrawalRequestPlan {
440 owner: RECEIVER,
441 receiver: OWNER,
442 shares,
443 expected_assets,
444 };
445
446 let requested =
447 apply_withdrawal_request_plan(state, &config, &SELF, plan, TimestampNs::ZERO).unwrap();
448
449 assert!(requested.state.op_state.is_idle());
450 assert_eq!(requested.state.idle_assets, before.idle_assets);
451 assert_eq!(requested.state.external_assets, before.external_assets);
452 assert_eq!(requested.state.total_assets, before.total_assets);
453 assert_eq!(requested.state.total_shares, before.total_shares);
454 assert_eq!(requested.state.next_op_id, before.next_op_id);
455 assert_eq!(requested.state.withdraw_queue.status().length, 1);
456 assert_eq!(
457 requested.state.withdraw_queue.status().total_escrow_shares,
458 shares
459 );
460 assert_eq!(
461 requested
462 .state
463 .withdraw_queue
464 .status()
465 .total_expected_assets,
466 expected_assets
467 );
468 let (request_id, head) = requested.state.withdraw_queue.head().unwrap();
469 assert_eq!(request_id, 0);
470 assert_address_eq(head.owner, RECEIVER);
471 assert_address_eq(head.receiver, OWNER);
472 assert_eq!(head.escrow_shares, shares);
473 assert_eq!(head.expected_assets, expected_assets);
474 assert_eq!(requested.effects.len(), 2);
475 assert_transfer_shares_effect(&requested.effects[0], RECEIVER, SELF, shares);
476 assert_emit_event_effect(&requested.effects[1]);
477 assert_asset_sum(&requested.state);
478 }
479
480 #[kani::proof]
481 #[kani::unwind(40)]
482 fn post_deposit_request_withdraw_preserves_accounting_and_escrows_previewed_shares() {
483 let deposited_assets = nonzero_bounded_amount();
484 let minted_shares = deposited_assets;
485 let config = zero_fee_config();
486 let post_deposit = VaultState::with_initial(
487 deposited_assets,
488 minted_shares,
489 deposited_assets,
490 0,
491 TimestampNs::from_nanos(1),
492 );
493 let post_deposit_idle_assets = post_deposit.idle_assets;
494 let post_deposit_external_assets = post_deposit.external_assets;
495 let post_deposit_total_assets = post_deposit.total_assets;
496 let post_deposit_total_shares = post_deposit.total_shares;
497 let post_deposit_next_op_id = post_deposit.next_op_id;
498 let expected_assets = deposited_assets;
499 let request_plan = WithdrawalRequestPlan {
500 owner: RECEIVER,
501 receiver: OWNER,
502 shares: minted_shares,
503 expected_assets,
504 };
505
506 let requested = apply_withdrawal_request_plan(
507 post_deposit,
508 &config,
509 &SELF,
510 request_plan,
511 TimestampNs::from_nanos(2),
512 )
513 .unwrap();
514
515 assert!(requested.state.op_state.is_idle());
516 assert_eq!(requested.state.idle_assets, post_deposit_idle_assets);
517 assert_eq!(
518 requested.state.external_assets,
519 post_deposit_external_assets
520 );
521 assert_eq!(requested.state.total_assets, post_deposit_total_assets);
522 assert_eq!(requested.state.total_shares, post_deposit_total_shares);
523 assert_eq!(requested.state.next_op_id, post_deposit_next_op_id);
524 assert_eq!(requested.state.withdraw_queue.status().length, 1);
525 assert_eq!(
526 requested.state.withdraw_queue.status().total_escrow_shares,
527 minted_shares
528 );
529 assert_eq!(
530 requested
531 .state
532 .withdraw_queue
533 .status()
534 .total_expected_assets,
535 expected_assets
536 );
537 let (request_id, head) = requested.state.withdraw_queue.head().unwrap();
538 assert_eq!(request_id, 0);
539 assert_address_eq(head.owner, RECEIVER);
540 assert_address_eq(head.receiver, OWNER);
541 assert_eq!(head.escrow_shares, minted_shares);
542 assert_eq!(head.expected_assets, expected_assets);
543 assert_eq!(requested.effects.len(), 2);
544 assert_transfer_shares_effect(&requested.effects[0], RECEIVER, SELF, minted_shares);
545 assert_emit_event_effect(&requested.effects[1]);
546 assert_asset_sum(&requested.state);
547 }
548
549 #[cfg(feature = "action-sync-external")]
550 #[kani::proof]
551 fn rebalance_withdraw_conserves_total_assets_and_moves_external_to_idle() {
552 let idle = bounded_amount();
553 let external = bounded_amount();
554 let shares = bounded_amount();
555 let amount = bounded_amount();
556 kani::assume(amount <= external);
557
558 let state =
559 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
560 let before_total_assets = state.total_assets;
561 let before_total_shares = state.total_shares;
562
563 let result = match apply_action(
564 state,
565 &zero_fee_config(),
566 None,
567 &SELF,
568 KernelAction::rebalance_withdraw(0, amount, TimestampNs::ZERO),
569 ) {
570 Ok(result) => result,
571 Err(_) => panic!("bounded rebalance withdraw should succeed"),
572 };
573
574 assert_eq!(
575 result.state.total_assets,
576 result.state.idle_assets + result.state.external_assets
577 );
578 assert_eq!(result.state.total_assets, before_total_assets);
579 assert_eq!(result.state.total_shares, before_total_shares);
580 assert_eq!(result.state.idle_assets, idle + amount);
581 assert_eq!(result.state.external_assets, external - amount);
582 }
583
584 #[cfg(feature = "action-sync-external")]
585 #[kani::proof]
586 fn sync_external_assets_preserves_total_as_idle_plus_external() {
587 let idle = bounded_amount();
588 let external = bounded_amount();
589 let synced_external = bounded_amount();
590 let shares = bounded_amount();
591 let op_id = 7;
592
593 let mut state =
594 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
595 state.op_state = OpState::Allocating(AllocatingState {
596 op_id,
597 index: 0,
598 remaining: 0,
599 plan: Vec::new(),
600 });
601
602 let result = match apply_action(
603 state,
604 &zero_fee_config(),
605 None,
606 &SELF,
607 KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO),
608 ) {
609 Ok(result) => result,
610 Err(_) => panic!("bounded sync external assets should succeed"),
611 };
612
613 assert_eq!(
614 result.state.total_assets,
615 result.state.idle_assets + result.state.external_assets
616 );
617 assert_eq!(result.state.idle_assets, idle);
618 assert_eq!(result.state.external_assets, synced_external);
619 assert_eq!(result.state.total_assets, idle + synced_external);
620 assert_eq!(result.state.total_shares, shares);
621 }
622
623 #[cfg(feature = "action-sync-external")]
624 #[kani::proof]
625 fn bounded_sync_then_rebalance_conserves_accounting_across_actions() {
626 let idle = bounded_amount();
627 let external = bounded_amount();
628 let shares = bounded_amount();
629 let synced_external = bounded_amount();
630 let rebalance_amount = bounded_amount();
631 let op_id = 9;
632 kani::assume(rebalance_amount <= synced_external);
633
634 let mut state =
635 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
636 state.op_state = OpState::Allocating(AllocatingState {
637 op_id,
638 index: 0,
639 remaining: 0,
640 plan: Vec::new(),
641 });
642
643 let synced = match apply_action(
644 state,
645 &zero_fee_config(),
646 None,
647 &SELF,
648 KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO),
649 ) {
650 Ok(result) => result.state,
651 Err(_) => panic!("bounded sync external assets should succeed"),
652 };
653
654 let rebalanced = match apply_action(
655 synced,
656 &zero_fee_config(),
657 None,
658 &SELF,
659 KernelAction::rebalance_withdraw(op_id, rebalance_amount, TimestampNs::ZERO),
660 ) {
661 Ok(result) => result.state,
662 Err(_) => panic!("bounded rebalance withdraw should succeed after sync"),
663 };
664
665 assert_eq!(
666 rebalanced.total_assets,
667 rebalanced.idle_assets + rebalanced.external_assets
668 );
669 assert_eq!(rebalanced.total_shares, shares);
670 assert_eq!(rebalanced.idle_assets, idle + rebalance_amount);
671 assert_eq!(
672 rebalanced.external_assets,
673 synced_external - rebalance_amount
674 );
675 assert_eq!(rebalanced.total_assets, idle + synced_external);
676 }
677
678 #[cfg(all(
679 feature = "action-allocation-lifecycle",
680 feature = "action-sync-external",
681 feature = "action-recovery"
682 ))]
683 #[kani::proof]
684 #[kani::unwind(8)]
685 fn allocation_partial_sync_then_abort_restores_unallocated_assets() {
686 let idle = nonzero_bounded_amount();
687 let external = bounded_amount();
688 let shares = bounded_amount();
689 let first = nonzero_bounded_amount();
690 let second = bounded_amount();
691 kani::assume(first + second <= idle);
692
693 let op_id = 11;
694 let state =
695 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
696 let started = apply_action(
697 state,
698 &zero_fee_config(),
699 None,
700 &SELF,
701 KernelAction::begin_allocating(
702 op_id,
703 allocation_plan(first, second),
704 TimestampNs::ZERO,
705 ),
706 )
707 .unwrap()
708 .state;
709
710 let stepped = allocation_step_callback(started.op_state.clone(), true, first, op_id)
711 .unwrap()
712 .new_state;
713 let mut after_step = started;
714 after_step.op_state = stepped;
715
716 let synced = apply_action(
717 after_step,
718 &zero_fee_config(),
719 None,
720 &SELF,
721 KernelAction::sync_external_assets(external + first, op_id, TimestampNs::ZERO),
722 )
723 .unwrap()
724 .state;
725
726 let result = apply_action(
727 synced,
728 &zero_fee_config(),
729 None,
730 &SELF,
731 KernelAction::abort_allocating(op_id),
732 )
733 .unwrap();
734
735 assert!(result.state.op_state.is_idle());
736 assert_asset_sum(&result.state);
737 assert_eq!(result.state.idle_assets, idle - first);
738 assert_eq!(result.state.external_assets, external + first);
739 assert_eq!(result.state.total_assets, idle + external);
740 assert_eq!(result.state.total_shares, shares);
741 assert_eq!(result.state.withdraw_queue.status().length, 0);
742 }
743
744 #[cfg(all(
745 feature = "action-allocation-lifecycle",
746 feature = "action-sync-external"
747 ))]
748 #[kani::proof]
749 #[kani::unwind(8)]
750 fn allocation_full_sync_then_finish_conserves_assets() {
751 let idle = nonzero_bounded_amount();
752 let external = bounded_amount();
753 let shares = bounded_amount();
754 let first = nonzero_bounded_amount();
755 let second = bounded_amount();
756 kani::assume(first + second <= idle);
757
758 let op_id = 12;
759 let state =
760 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
761 let started = apply_action(
762 state,
763 &zero_fee_config(),
764 None,
765 &SELF,
766 KernelAction::begin_allocating(
767 op_id,
768 allocation_plan(first, second),
769 TimestampNs::ZERO,
770 ),
771 )
772 .unwrap()
773 .state;
774
775 let stepped_once = allocation_step_callback(started.op_state.clone(), true, first, op_id)
776 .unwrap()
777 .new_state;
778 let stepped_twice = if second > 0 {
779 allocation_step_callback(stepped_once, true, second, op_id)
780 .unwrap()
781 .new_state
782 } else {
783 stepped_once
784 };
785 let mut after_steps = started;
786 after_steps.op_state = stepped_twice;
787
788 let synced = apply_action(
789 after_steps,
790 &zero_fee_config(),
791 None,
792 &SELF,
793 KernelAction::sync_external_assets(external + first + second, op_id, TimestampNs::ZERO),
794 )
795 .unwrap()
796 .state;
797
798 let result = apply_action(
799 synced,
800 &zero_fee_config(),
801 None,
802 &SELF,
803 KernelAction::finish_allocating(op_id, TimestampNs::ZERO),
804 )
805 .unwrap();
806
807 assert!(result.state.op_state.is_idle());
808 assert_asset_sum(&result.state);
809 assert_eq!(result.state.idle_assets, idle - first - second);
810 assert_eq!(result.state.external_assets, external + first + second);
811 assert_eq!(result.state.total_assets, idle + external);
812 assert_eq!(result.state.total_shares, shares);
813 }
814
815 #[cfg(all(
816 feature = "action-allocation-lifecycle",
817 feature = "action-sync-external",
818 feature = "action-recovery"
819 ))]
820 #[kani::proof]
821 fn allocation_wrong_op_id_is_rejected_without_progress() {
822 let mut state = bounded_state();
823 let op_id = 13;
824 let wrong_op_id = 14;
825 state.op_state = OpState::Allocating(AllocatingState {
826 op_id,
827 index: 0,
828 remaining: 1,
829 plan: allocation_plan(1, 0),
830 });
831 let baseline = state.clone();
832
833 assert!(allocation_step_callback(state.op_state.clone(), true, 1, wrong_op_id).is_err());
834 assert!(apply_action(
835 state.clone(),
836 &zero_fee_config(),
837 None,
838 &SELF,
839 KernelAction::sync_external_assets(1, wrong_op_id, TimestampNs::ZERO),
840 )
841 .is_err());
842 assert!(apply_action(
843 state.clone(),
844 &zero_fee_config(),
845 None,
846 &SELF,
847 KernelAction::finish_allocating(wrong_op_id, TimestampNs::ZERO),
848 )
849 .is_err());
850 assert!(apply_action(
851 state.clone(),
852 &zero_fee_config(),
853 None,
854 &SELF,
855 KernelAction::abort_allocating(wrong_op_id),
856 )
857 .is_err());
858 assert!(state == baseline);
859 }
860
861 #[kani::proof]
862 fn withdrawal_collection_preserves_collected_plus_remaining() {
863 let amount = nonzero_bounded_amount();
864 let first_collect = bounded_amount();
865 let burn_shares = bounded_amount();
866 let escrow_shares = nonzero_bounded_amount();
867 kani::assume(first_collect <= amount);
868 kani::assume(burn_shares <= escrow_shares);
869
870 let op_id = 31;
871 let request = WithdrawalRequest {
872 op_id,
873 request_id: 0,
874 amount,
875 receiver: RECEIVER,
876 owner: OWNER,
877 escrow_shares,
878 };
879
880 let started = start_withdrawal(OpState::Idle, request).unwrap().new_state;
881 let stepped = withdrawal_step_callback(started, op_id, first_collect)
882 .unwrap()
883 .new_state;
884 let withdrawing = stepped.as_withdrawing().unwrap();
885 assert_eq!(withdrawing.collected + withdrawing.remaining, amount);
886
887 if withdrawing.remaining > 0 {
888 assert!(withdrawal_collected(stepped.clone(), op_id, burn_shares).is_err());
889 }
890
891 let completed = withdrawal_step_callback(stepped, op_id, amount - first_collect)
892 .unwrap()
893 .new_state;
894 let payout = withdrawal_collected(completed, op_id, burn_shares)
895 .unwrap()
896 .new_state;
897 let payout = payout.as_payout().unwrap();
898 assert_eq!(payout.amount, amount);
899 assert_eq!(payout.burn_shares, burn_shares);
900 assert!(payout.burn_shares <= payout.escrow_shares);
901 }
902
903 #[kani::proof]
904 #[kani::unwind(40)]
905 fn withdrawal_queue_head_validation_requires_exact_identity_fields() {
906 let mut state = VaultState::with_initial(16, 16, 16, 0, TimestampNs::ZERO);
907 let first_id = enqueue_withdrawal(&mut state, OWNER, RECEIVER, 3, 5, TimestampNs::ZERO);
908
909 assert!(
910 validate_queue_head(&state.withdraw_queue, first_id, &OWNER, &RECEIVER, 3,).is_ok()
911 );
912 assert!(
913 validate_queue_head(&state.withdraw_queue, first_id + 1, &OWNER, &RECEIVER, 3,)
914 .is_err()
915 );
916 assert!(
917 validate_queue_head(&state.withdraw_queue, first_id, &SECOND_OWNER, &RECEIVER, 3,)
918 .is_err()
919 );
920 assert!(
921 validate_queue_head(&state.withdraw_queue, first_id, &OWNER, &SECOND_RECEIVER, 3,)
922 .is_err()
923 );
924 assert!(
925 validate_queue_head(&state.withdraw_queue, first_id, &OWNER, &RECEIVER, 4,).is_err()
926 );
927 assert_eq!(
928 state.withdraw_queue.head().map(|(id, _)| id),
929 Some(first_id)
930 );
931 }
932
933 #[kani::proof]
934 #[kani::unwind(40)]
935 fn withdrawal_queue_head_validation_rejects_later_fifo_entry() {
936 let mut state = VaultState::with_initial(16, 16, 16, 0, TimestampNs::ZERO);
937 let first_id = enqueue_withdrawal(&mut state, OWNER, RECEIVER, 3, 5, TimestampNs::ZERO);
938 let second_id = enqueue_withdrawal(
939 &mut state,
940 SECOND_OWNER,
941 SECOND_RECEIVER,
942 7,
943 11,
944 TimestampNs::ZERO,
945 );
946 let before = state.withdraw_queue.status();
947
948 assert!(
949 validate_queue_head(&state.withdraw_queue, first_id, &OWNER, &RECEIVER, 3,).is_ok()
950 );
951 assert!(validate_queue_head(
952 &state.withdraw_queue,
953 second_id,
954 &SECOND_OWNER,
955 &SECOND_RECEIVER,
956 7,
957 )
958 .is_err());
959 assert_eq!(
960 state.withdraw_queue.head().map(|(id, _)| id),
961 Some(first_id)
962 );
963 assert_eq!(state.withdraw_queue.status().length, before.length);
964 assert_eq!(
965 state.withdraw_queue.status().total_escrow_shares,
966 before.total_escrow_shares
967 );
968 assert_eq!(
969 state.withdraw_queue.status().total_expected_assets,
970 before.total_expected_assets
971 );
972 }
973
974 #[kani::proof]
975 #[kani::unwind(40)]
976 fn withdrawal_fifo_head_maps_to_started_withdrawal_request() {
977 let mut state = VaultState::with_initial(16, 16, 16, 0, TimestampNs::ZERO);
978 let first_id = enqueue_withdrawal(&mut state, OWNER, RECEIVER, 3, 5, TimestampNs::ZERO);
979
980 let head = pending_withdrawal_head(&state).unwrap();
981 assert_eq!(head.id, first_id);
982 assert_address_eq(head.owner, OWNER);
983 assert_address_eq(head.receiver, RECEIVER);
984 assert_eq!(head.escrow_shares, 3);
985 assert_eq!(head.expected_assets, 5);
986
987 let request = withdrawal_request_from_head(&mut state, head);
988 assert_eq!(request.request_id, first_id);
989 assert_address_eq(request.owner, OWNER);
990 assert_address_eq(request.receiver, RECEIVER);
991 assert_eq!(request.escrow_shares, 3);
992 assert_eq!(request.amount, 5);
993 assert_eq!(state.withdraw_queue.status().length, 1);
994
995 let started = start_withdrawal(OpState::Idle, request).unwrap().new_state;
996 let withdrawing = started.as_withdrawing().unwrap();
997 assert_eq!(withdrawing.request_id, first_id);
998 assert_address_eq(withdrawing.owner, OWNER);
999 assert_address_eq(withdrawing.receiver, RECEIVER);
1000 assert_eq!(withdrawing.escrow_shares, 3);
1001 assert_eq!(withdrawing.remaining, 5);
1002 }
1003
1004 #[kani::proof]
1005 #[kani::unwind(40)]
1006 fn payout_queue_head_dequeues_once_before_settlement() {
1007 let mut queue = WithdrawQueue::new();
1008 let first_id = queue
1009 .enqueue(OWNER, RECEIVER, 3, 5, TimestampNs::ZERO, 3)
1010 .unwrap();
1011 let second_id = queue
1012 .enqueue(SECOND_OWNER, SECOND_RECEIVER, 7, 11, TimestampNs::ZERO, 3)
1013 .unwrap();
1014
1015 let (dequeued_id, dequeued) = queue.dequeue().unwrap();
1016 assert_eq!(dequeued_id, first_id);
1017 assert_address_eq(dequeued.owner, OWNER);
1018 assert_address_eq(dequeued.receiver, RECEIVER);
1019 assert_eq!(dequeued.escrow_shares, 3);
1020 assert_eq!(dequeued.expected_assets, 5);
1021 assert_eq!(queue.status().length, 1);
1022 assert_eq!(queue.status().total_escrow_shares, 7);
1023 assert_eq!(queue.status().total_expected_assets, 11);
1024 assert_eq!(queue.head().map(|(id, _)| id), Some(second_id));
1025 }
1026
1027 #[kani::proof]
1028 #[kani::unwind(40)]
1029 fn payout_success_settlement_conserves_assets_and_escrow() {
1030 let idle = nonzero_bounded_amount();
1031 let external = bounded_amount();
1032 let total_shares = nonzero_bounded_amount();
1033 let escrow_shares = nonzero_bounded_amount();
1034 let burn_shares = bounded_amount();
1035 let amount = bounded_amount();
1036 kani::assume(burn_shares <= escrow_shares);
1037 kani::assume(burn_shares <= total_shares);
1038 kani::assume(amount <= idle);
1039
1040 let op_id = 41;
1041 let mut state = VaultState::with_initial(
1042 idle + external,
1043 total_shares,
1044 idle,
1045 external,
1046 TimestampNs::ZERO,
1047 );
1048 let request_id = enqueue_withdrawal(
1049 &mut state,
1050 OWNER,
1051 RECEIVER,
1052 escrow_shares,
1053 amount,
1054 TimestampNs::ZERO,
1055 );
1056 let payout = PayoutState {
1057 op_id,
1058 request_id,
1059 receiver: RECEIVER,
1060 amount,
1061 owner: OWNER,
1062 escrow_shares,
1063 burn_shares,
1064 };
1065
1066 assert!(validate_queue_head(
1067 &state.withdraw_queue,
1068 payout.request_id,
1069 &payout.owner,
1070 &payout.receiver,
1071 payout.escrow_shares,
1072 )
1073 .is_ok());
1074 let (dequeued_id, dequeued) = state.withdraw_queue.dequeue().unwrap();
1075 assert_eq!(dequeued_id, request_id);
1076 assert_address_eq(dequeued.owner, OWNER);
1077 assert_address_eq(dequeued.receiver, RECEIVER);
1078 assert_eq!(dequeued.escrow_shares, escrow_shares);
1079 assert_eq!(state.withdraw_queue.status().length, 0);
1080
1081 let settlement = plan_payout_settlement(&payout, PayoutOutcome::Success).unwrap();
1082 let mut effects = Vec::new();
1083 apply_payout_settlement(&mut state, &payout, settlement, SELF, &mut effects).unwrap();
1084
1085 assert!(state.op_state.is_idle());
1086 assert_asset_sum(&state);
1087 assert!(settlement.success);
1088 assert_eq!(settlement.burn_shares, burn_shares);
1089 assert_eq!(settlement.refund_shares, escrow_shares - burn_shares);
1090 assert_eq!(
1091 settlement.burn_shares + settlement.refund_shares,
1092 escrow_shares
1093 );
1094 assert_eq!(settlement.completed_amount, amount);
1095 assert_eq!(state.idle_assets, idle - amount);
1096 assert_eq!(state.external_assets, external);
1097 assert_eq!(state.total_assets, idle + external - amount);
1098 assert_eq!(state.total_shares, total_shares - burn_shares);
1099 assert_eq!(state.withdraw_queue.status().length, 0);
1100 }
1101
1102 #[kani::proof]
1103 #[kani::unwind(40)]
1104 fn payout_failure_settlement_refunds_without_mutating_assets_or_shares_and_dequeues_head_once()
1105 {
1106 let idle = nonzero_bounded_amount();
1107 let external = bounded_amount();
1108 let total_shares = nonzero_bounded_amount();
1109 let escrow_shares = nonzero_bounded_amount();
1110 let burn_shares = bounded_amount();
1111 let amount = bounded_amount();
1112 kani::assume(burn_shares <= escrow_shares);
1113 kani::assume(amount <= idle);
1114
1115 let op_id = 42;
1116 let mut state = VaultState::with_initial(
1117 idle + external,
1118 total_shares,
1119 idle,
1120 external,
1121 TimestampNs::ZERO,
1122 );
1123 let request_id = enqueue_withdrawal(
1124 &mut state,
1125 OWNER,
1126 RECEIVER,
1127 escrow_shares,
1128 amount,
1129 TimestampNs::ZERO,
1130 );
1131 let payout = PayoutState {
1132 op_id,
1133 request_id,
1134 receiver: RECEIVER,
1135 amount,
1136 owner: OWNER,
1137 escrow_shares,
1138 burn_shares,
1139 };
1140
1141 assert!(validate_queue_head(
1142 &state.withdraw_queue,
1143 payout.request_id,
1144 &payout.owner,
1145 &payout.receiver,
1146 payout.escrow_shares,
1147 )
1148 .is_ok());
1149 let (dequeued_id, dequeued) = state.withdraw_queue.dequeue().unwrap();
1150 assert_eq!(dequeued_id, request_id);
1151 assert_address_eq(dequeued.owner, OWNER);
1152 assert_address_eq(dequeued.receiver, RECEIVER);
1153 assert_eq!(dequeued.escrow_shares, escrow_shares);
1154 assert_eq!(state.withdraw_queue.status().length, 0);
1155
1156 let settlement = plan_payout_settlement(&payout, PayoutOutcome::Failure).unwrap();
1157 let mut effects = Vec::new();
1158 apply_payout_settlement(&mut state, &payout, settlement, SELF, &mut effects).unwrap();
1159
1160 assert!(state.op_state.is_idle());
1161 assert_asset_sum(&state);
1162 assert!(!settlement.success);
1163 assert_eq!(settlement.burn_shares, 0);
1164 assert_eq!(settlement.refund_shares, escrow_shares);
1165 assert_eq!(settlement.completed_amount, 0);
1166 assert_eq!(state.idle_assets, idle);
1167 assert_eq!(state.external_assets, external);
1168 assert_eq!(state.total_assets, idle + external);
1169 assert_eq!(state.total_shares, total_shares);
1170 }
1171
1172 #[cfg(feature = "action-recovery")]
1173 #[kani::proof]
1174 #[kani::unwind(8)]
1175 fn emergency_reset_allocating_restores_remaining_assets_to_idle() {
1176 let idle = bounded_amount();
1177 let external = bounded_amount();
1178 let total_shares = bounded_amount();
1179 let remaining = bounded_amount();
1180 let op_id = 51;
1181
1182 let mut state = VaultState::with_initial(
1183 idle + external,
1184 total_shares,
1185 idle,
1186 external,
1187 TimestampNs::ZERO,
1188 );
1189 state.op_state = OpState::Allocating(AllocatingState {
1190 op_id,
1191 index: 0,
1192 remaining,
1193 plan: allocation_plan(remaining, 0),
1194 });
1195
1196 let result = plan_emergency_reset(state).unwrap();
1197
1198 assert!(result.state.op_state.is_idle());
1199 assert_eq!(result.state.idle_assets, idle + remaining);
1200 assert_eq!(result.state.external_assets, external);
1201 assert_eq!(result.state.total_assets, idle + external + remaining);
1202 assert_eq!(result.state.total_shares, total_shares);
1203 assert_eq!(result.state.withdraw_queue.status().length, 0);
1204 assert!(result.refund_owner.is_none());
1205 assert_eq!(result.refund_shares, 0);
1206 assert_eq!(
1207 result.state.fee_anchor.total_assets,
1208 result.state.total_assets
1209 );
1210 assert_asset_sum(&result.state);
1211 }
1212
1213 #[cfg(feature = "action-recovery")]
1214 #[kani::proof]
1215 #[kani::unwind(8)]
1216 fn emergency_reset_withdrawing_restores_collected_assets_and_refunds_escrow() {
1217 let idle = bounded_amount();
1218 let external = bounded_amount();
1219 let total_shares = nonzero_bounded_amount();
1220 let remaining = bounded_amount();
1221 let collected = bounded_amount();
1222 let escrow_shares = nonzero_bounded_amount();
1223 let op_id = 52;
1224
1225 let mut state = VaultState::with_initial(
1226 idle + external,
1227 total_shares,
1228 idle,
1229 external,
1230 TimestampNs::ZERO,
1231 );
1232 let request_id = enqueue_withdrawal(
1233 &mut state,
1234 OWNER,
1235 RECEIVER,
1236 escrow_shares,
1237 collected + remaining,
1238 TimestampNs::ZERO,
1239 );
1240 state.op_state = OpState::Withdrawing(WithdrawingState {
1241 op_id,
1242 request_id,
1243 index: 0,
1244 remaining,
1245 collected,
1246 receiver: RECEIVER,
1247 owner: OWNER,
1248 escrow_shares,
1249 });
1250
1251 let result = plan_emergency_reset(state).unwrap();
1252
1253 assert!(result.state.op_state.is_idle());
1254 assert_eq!(result.state.idle_assets, idle + collected);
1255 assert_eq!(result.state.external_assets, external);
1256 assert_eq!(result.state.total_assets, idle + external + collected);
1257 assert_eq!(result.state.total_shares, total_shares);
1258 assert_eq!(result.state.withdraw_queue.status().length, 0);
1259 assert_refund_owner_is_owner(result.refund_owner);
1260 assert_eq!(result.refund_shares, escrow_shares);
1261 assert_eq!(
1262 result.state.fee_anchor.total_assets,
1263 result.state.total_assets
1264 );
1265 assert_asset_sum(&result.state);
1266 }
1267
1268 #[cfg(feature = "action-recovery")]
1269 #[kani::proof]
1270 #[kani::unwind(8)]
1271 fn emergency_reset_payout_restores_payout_assets_and_refunds_escrow() {
1272 let idle = bounded_amount();
1273 let external = bounded_amount();
1274 let total_shares = nonzero_bounded_amount();
1275 let amount = bounded_amount();
1276 let escrow_shares = nonzero_bounded_amount();
1277 let burn_shares = bounded_amount();
1278 let op_id = 53;
1279 kani::assume(burn_shares <= escrow_shares);
1280
1281 let mut state = VaultState::with_initial(
1282 idle + external,
1283 total_shares,
1284 idle,
1285 external,
1286 TimestampNs::ZERO,
1287 );
1288 let request_id = enqueue_withdrawal(
1289 &mut state,
1290 OWNER,
1291 RECEIVER,
1292 escrow_shares,
1293 amount,
1294 TimestampNs::ZERO,
1295 );
1296 state.op_state = OpState::Payout(PayoutState {
1297 op_id,
1298 request_id,
1299 receiver: RECEIVER,
1300 amount,
1301 owner: OWNER,
1302 escrow_shares,
1303 burn_shares,
1304 });
1305
1306 let result = plan_emergency_reset(state).unwrap();
1307
1308 assert!(result.state.op_state.is_idle());
1309 assert_eq!(result.state.idle_assets, idle + amount);
1310 assert_eq!(result.state.external_assets, external);
1311 assert_eq!(result.state.total_assets, idle + external + amount);
1312 assert_eq!(result.state.total_shares, total_shares);
1313 assert_eq!(result.state.withdraw_queue.status().length, 0);
1314 assert_refund_owner_is_owner(result.refund_owner);
1315 assert_eq!(result.refund_shares, escrow_shares);
1316 assert_eq!(
1317 result.state.fee_anchor.total_assets,
1318 result.state.total_assets
1319 );
1320 assert_asset_sum(&result.state);
1321 }
1322
1323 #[cfg(feature = "action-recovery")]
1324 #[kani::proof]
1325 #[kani::unwind(8)]
1326 fn emergency_reset_refreshing_returns_idle_without_accounting_mutation() {
1327 let idle = bounded_amount();
1328 let external = bounded_amount();
1329 let total_shares = bounded_amount();
1330 let op_id = 54;
1331
1332 let mut state = VaultState::with_initial(
1333 idle + external,
1334 total_shares,
1335 idle,
1336 external,
1337 TimestampNs::ZERO,
1338 );
1339 let before = state.clone();
1340 state.op_state = OpState::Refreshing(RefreshingState {
1341 op_id,
1342 index: 1,
1343 plan: vec![7, 8],
1344 });
1345
1346 let result = plan_emergency_reset(state).unwrap();
1347
1348 assert!(result.state.op_state.is_idle());
1349 assert_eq!(result.state.idle_assets, before.idle_assets);
1350 assert_eq!(result.state.external_assets, before.external_assets);
1351 assert_eq!(result.state.total_assets, before.total_assets);
1352 assert_eq!(result.state.total_shares, before.total_shares);
1353 assert_eq!(
1354 result.state.withdraw_queue.status().length,
1355 before.withdraw_queue.status().length
1356 );
1357 assert!(result.refund_owner.is_none());
1358 assert_eq!(result.refund_shares, 0);
1359 assert_eq!(
1360 result.state.fee_anchor.total_assets,
1361 result.state.total_assets
1362 );
1363 assert_asset_sum(&result.state);
1364 }
1365
1366 #[cfg(feature = "action-sync-external")]
1367 #[kani::proof]
1368 #[kani::unwind(8)]
1369 fn sync_external_assets_allocating_only_mutates_external_and_total_assets() {
1370 let idle = bounded_amount();
1371 let external = bounded_amount();
1372 let synced_external = bounded_amount();
1373 let shares = bounded_amount();
1374 let op_id = 61;
1375
1376 let mut state =
1377 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
1378 state.op_state = OpState::Allocating(AllocatingState {
1379 op_id,
1380 index: 1,
1381 remaining: 2,
1382 plan: allocation_plan(1, 1),
1383 });
1384
1385 let before_idle = state.idle_assets;
1386 let before_shares = state.total_shares;
1387 let before_queue = state.withdraw_queue.status();
1388 let before_next_op_id = state.next_op_id;
1389 let before_fee_anchor_total_assets = state.fee_anchor.total_assets;
1390 let before_fee_anchor_timestamp = state.fee_anchor.timestamp_ns;
1391 let result = apply_action(
1392 state,
1393 &zero_fee_config(),
1394 None,
1395 &SELF,
1396 KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO),
1397 )
1398 .unwrap();
1399
1400 assert_eq!(result.state.idle_assets, before_idle);
1401 assert_eq!(result.state.external_assets, synced_external);
1402 assert_eq!(result.state.total_assets, before_idle + synced_external);
1403 assert_eq!(result.state.total_shares, before_shares);
1404 assert_eq!(
1405 result.state.withdraw_queue.status().length,
1406 before_queue.length
1407 );
1408 assert_eq!(
1409 result.state.withdraw_queue.status().total_escrow_shares,
1410 before_queue.total_escrow_shares
1411 );
1412 assert_eq!(
1413 result.state.withdraw_queue.status().total_expected_assets,
1414 before_queue.total_expected_assets
1415 );
1416 assert_eq!(result.state.next_op_id, before_next_op_id);
1417 assert_eq!(
1418 result.state.fee_anchor.total_assets,
1419 before_fee_anchor_total_assets
1420 );
1421 assert!(result.state.fee_anchor.timestamp_ns == before_fee_anchor_timestamp);
1422 if let OpState::Allocating(alloc) = &result.state.op_state {
1423 assert_eq!(alloc.op_id, op_id);
1424 assert_eq!(alloc.index, 1);
1425 assert_eq!(alloc.remaining, 2);
1426 } else {
1427 panic!("sync must preserve allocating operation");
1428 }
1429 assert_asset_sum(&result.state);
1430 }
1431
1432 #[cfg(feature = "action-sync-external")]
1433 #[kani::proof]
1434 #[kani::unwind(8)]
1435 fn sync_external_assets_withdrawing_preserves_share_supply_queue_and_actor_fields() {
1436 let idle = bounded_amount();
1437 let external = bounded_amount();
1438 let synced_external = bounded_amount();
1439 let shares = bounded_amount();
1440 let op_id = 62;
1441
1442 let mut state =
1443 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
1444 state.op_state = OpState::Withdrawing(WithdrawingState {
1445 op_id,
1446 request_id: 7,
1447 index: 1,
1448 remaining: 2,
1449 collected: 2,
1450 receiver: RECEIVER,
1451 owner: OWNER,
1452 escrow_shares: 3,
1453 });
1454
1455 let before_queue = state.withdraw_queue.status();
1456 let before_next_op_id = state.next_op_id;
1457 let result = apply_action(
1458 state,
1459 &zero_fee_config(),
1460 None,
1461 &SELF,
1462 KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO),
1463 )
1464 .unwrap();
1465
1466 assert_eq!(result.state.idle_assets, idle);
1467 assert_eq!(result.state.external_assets, synced_external);
1468 assert_eq!(result.state.total_assets, idle + synced_external);
1469 assert_eq!(result.state.total_shares, shares);
1470 assert_eq!(
1471 result.state.withdraw_queue.status().length,
1472 before_queue.length
1473 );
1474 assert_eq!(
1475 result.state.withdraw_queue.status().total_escrow_shares,
1476 before_queue.total_escrow_shares
1477 );
1478 assert_eq!(
1479 result.state.withdraw_queue.status().total_expected_assets,
1480 before_queue.total_expected_assets
1481 );
1482 assert_eq!(result.state.next_op_id, before_next_op_id);
1483 if let OpState::Withdrawing(withdraw) = &result.state.op_state {
1484 assert_eq!(withdraw.op_id, op_id);
1485 assert_eq!(withdraw.request_id, 7);
1486 assert_eq!(withdraw.index, 1);
1487 assert_eq!(withdraw.remaining, 2);
1488 assert_eq!(withdraw.collected, 2);
1489 assert_address_eq(withdraw.owner, OWNER);
1490 assert_address_eq(withdraw.receiver, RECEIVER);
1491 assert_eq!(withdraw.escrow_shares, 3);
1492 } else {
1493 panic!("sync must preserve withdrawing operation");
1494 }
1495 assert_asset_sum(&result.state);
1496 }
1497
1498 #[cfg(feature = "action-sync-external")]
1499 #[kani::proof]
1500 #[kani::unwind(8)]
1501 fn sync_external_assets_refreshing_only_mutates_external_and_total_assets() {
1502 let idle = bounded_amount();
1503 let external = bounded_amount();
1504 let synced_external = bounded_amount();
1505 let shares = bounded_amount();
1506 let op_id = 63;
1507
1508 let mut state =
1509 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
1510 state.op_state = OpState::Refreshing(RefreshingState {
1511 op_id,
1512 index: 1,
1513 plan: vec![7, 8],
1514 });
1515
1516 let before_queue = state.withdraw_queue.status();
1517 let before_next_op_id = state.next_op_id;
1518 let result = apply_action(
1519 state,
1520 &zero_fee_config(),
1521 None,
1522 &SELF,
1523 KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO),
1524 )
1525 .unwrap();
1526
1527 assert_eq!(result.state.idle_assets, idle);
1528 assert_eq!(result.state.external_assets, synced_external);
1529 assert_eq!(result.state.total_assets, idle + synced_external);
1530 assert_eq!(result.state.total_shares, shares);
1531 assert_eq!(
1532 result.state.withdraw_queue.status().length,
1533 before_queue.length
1534 );
1535 assert_eq!(
1536 result.state.withdraw_queue.status().total_escrow_shares,
1537 before_queue.total_escrow_shares
1538 );
1539 assert_eq!(
1540 result.state.withdraw_queue.status().total_expected_assets,
1541 before_queue.total_expected_assets
1542 );
1543 assert_eq!(result.state.next_op_id, before_next_op_id);
1544 if let OpState::Refreshing(refresh) = &result.state.op_state {
1545 assert_eq!(refresh.op_id, op_id);
1546 assert_eq!(refresh.index, 1);
1547 } else {
1548 panic!("sync must preserve refreshing operation");
1549 }
1550 assert_asset_sum(&result.state);
1551 }
1552
1553 #[cfg(feature = "action-sync-external")]
1554 #[kani::proof]
1555 #[kani::unwind(8)]
1556 fn sync_external_assets_rejects_wrong_op_id_and_disallowed_states() {
1557 let idle = bounded_amount();
1558 let external = bounded_amount();
1559 let synced_external = bounded_amount();
1560 let shares = bounded_amount();
1561 let op_id = 64;
1562
1563 let mut allocating =
1564 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
1565 allocating.op_state = OpState::Allocating(AllocatingState {
1566 op_id,
1567 index: 1,
1568 remaining: 2,
1569 plan: allocation_plan(1, 1),
1570 });
1571 assert!(apply_action(
1572 allocating,
1573 &zero_fee_config(),
1574 None,
1575 &SELF,
1576 KernelAction::sync_external_assets(synced_external, op_id + 1, TimestampNs::ZERO),
1577 )
1578 .is_err());
1579
1580 let idle_state =
1581 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
1582 assert!(apply_action(
1583 idle_state,
1584 &zero_fee_config(),
1585 None,
1586 &SELF,
1587 KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO),
1588 )
1589 .is_err());
1590
1591 let mut payout_state =
1592 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
1593 payout_state.op_state = OpState::Payout(PayoutState {
1594 op_id,
1595 request_id: 0,
1596 receiver: RECEIVER,
1597 amount: 1,
1598 owner: OWNER,
1599 escrow_shares: 1,
1600 burn_shares: 1,
1601 });
1602 assert!(apply_action(
1603 payout_state,
1604 &zero_fee_config(),
1605 None,
1606 &SELF,
1607 KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO),
1608 )
1609 .is_err());
1610 }
1611
1612 #[cfg(all(feature = "action-refresh-lifecycle", feature = "action-sync-external"))]
1613 #[kani::proof]
1614 #[kani::unwind(8)]
1615 fn refresh_lifecycle_mutates_only_external_assets_and_returns_idle() {
1616 let idle = bounded_amount();
1617 let external = bounded_amount();
1618 let synced_external = bounded_amount();
1619 let shares = bounded_amount();
1620 let op_id = 71;
1621
1622 let state =
1623 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
1624 let started = apply_action(
1625 state,
1626 &zero_fee_config(),
1627 None,
1628 &SELF,
1629 KernelAction::begin_refreshing(op_id, vec![1, 2], TimestampNs::ZERO),
1630 )
1631 .unwrap()
1632 .state;
1633 assert!(started.op_state.is_refreshing());
1634 assert_eq!(started.idle_assets, idle);
1635 assert_eq!(started.external_assets, external);
1636 assert_eq!(started.total_assets, idle + external);
1637 assert_eq!(started.total_shares, shares);
1638
1639 let synced = apply_action(
1640 started,
1641 &zero_fee_config(),
1642 None,
1643 &SELF,
1644 KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO),
1645 )
1646 .unwrap()
1647 .state;
1648
1649 let result = apply_action(
1650 synced,
1651 &zero_fee_config(),
1652 None,
1653 &SELF,
1654 KernelAction::finish_refreshing(op_id, TimestampNs::ZERO),
1655 )
1656 .unwrap();
1657
1658 assert!(result.state.op_state.is_idle());
1659 assert_eq!(result.state.idle_assets, idle);
1660 assert_eq!(result.state.external_assets, synced_external);
1661 assert_eq!(result.state.total_assets, idle + synced_external);
1662 assert_eq!(result.state.total_shares, shares);
1663 assert_asset_sum(&result.state);
1664 }
1665
1666 #[cfg(feature = "action-refresh-fees")]
1667 #[kani::proof]
1668 #[kani::unwind(8)]
1669 fn refresh_fees_zero_fee_rates_only_update_anchor() {
1670 let idle = bounded_amount();
1671 let external = bounded_amount();
1672 let shares = nonzero_bounded_amount();
1673 let anchor_assets = bounded_amount();
1674 let now = TimestampNs::from_nanos(1);
1675
1676 let mut state =
1677 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
1678 state.fee_anchor = FeeAccrualAnchor::new(anchor_assets, TimestampNs::ZERO);
1679 let before = state.clone();
1680 let before_queue = before.withdraw_queue.status();
1681
1682 let result = apply_action(
1683 state,
1684 &zero_fee_config(),
1685 None,
1686 &SELF,
1687 KernelAction::refresh_fees(now),
1688 )
1689 .unwrap();
1690
1691 assert_eq!(result.state.idle_assets, before.idle_assets);
1692 assert_eq!(result.state.external_assets, before.external_assets);
1693 assert_eq!(result.state.total_assets, before.total_assets);
1694 assert_eq!(result.effects.len(), 1);
1695 assert_emit_event_effect(&result.effects[0]);
1696 assert_eq!(result.state.total_shares, before.total_shares);
1697 assert_eq!(
1698 result.state.fee_anchor.total_assets,
1699 result.state.total_assets
1700 );
1701 assert!(result.state.fee_anchor.timestamp_ns == now);
1702 assert!(result.state.fee_anchor.timestamp_ns > before.fee_anchor.timestamp_ns);
1703 assert!(result.state.op_state.is_idle());
1704 assert_eq!(
1705 result.state.withdraw_queue.status().length,
1706 before_queue.length
1707 );
1708 assert_eq!(
1709 result.state.withdraw_queue.status().total_escrow_shares,
1710 before_queue.total_escrow_shares
1711 );
1712 assert_eq!(
1713 result.state.withdraw_queue.status().total_expected_assets,
1714 before_queue.total_expected_assets
1715 );
1716 assert_eq!(result.state.next_op_id, before.next_op_id);
1717 assert_asset_sum(&result.state);
1718 }
1719
1720 #[cfg(feature = "action-refresh-fees")]
1721 #[kani::proof]
1722 #[kani::unwind(8)]
1723 fn refresh_fees_active_rates_only_mint_fee_shares_and_update_anchor() {
1724 let idle = 100u128;
1725 let external = 0u128;
1726 let shares = 100u128;
1727 let anchor_assets = 0u128;
1728 let now = TimestampNs::from_nanos(1);
1729
1730 let mut state =
1731 VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO);
1732 state.fee_anchor = FeeAccrualAnchor::new(anchor_assets, TimestampNs::ZERO);
1733 let before = state.clone();
1734 let before_queue = before.withdraw_queue.status();
1735
1736 let result = apply_action(
1737 state,
1738 &active_fee_config(),
1739 None,
1740 &SELF,
1741 KernelAction::refresh_fees(now),
1742 )
1743 .unwrap();
1744
1745 assert_eq!(result.effects.len(), 2);
1746 let minted = assert_mint_shares_effect(&result.effects[0]);
1747 assert_emit_event_effect(&result.effects[1]);
1748
1749 assert!(minted > 0);
1750 assert_eq!(result.state.idle_assets, before.idle_assets);
1751 assert_eq!(result.state.external_assets, before.external_assets);
1752 assert_eq!(result.state.total_assets, before.total_assets);
1753 assert!(result.state.total_shares >= before.total_shares);
1754 assert_eq!(result.state.total_shares, before.total_shares + minted);
1755 assert_eq!(
1756 result.state.fee_anchor.total_assets,
1757 result.state.total_assets
1758 );
1759 assert!(result.state.fee_anchor.timestamp_ns == now);
1760 assert!(result.state.fee_anchor.timestamp_ns > before.fee_anchor.timestamp_ns);
1761 assert!(result.state.op_state.is_idle());
1762 assert_eq!(
1763 result.state.withdraw_queue.status().length,
1764 before_queue.length
1765 );
1766 assert_eq!(
1767 result.state.withdraw_queue.status().total_escrow_shares,
1768 before_queue.total_escrow_shares
1769 );
1770 assert_eq!(
1771 result.state.withdraw_queue.status().total_expected_assets,
1772 before_queue.total_expected_assets
1773 );
1774 assert_eq!(result.state.next_op_id, before.next_op_id);
1775 assert_asset_sum(&result.state);
1776 }
1777}
1778pub use types::{ActualIdx, Address, AssetId, DurationNs, ExpectedIdx, KernelVersion, TimestampNs};
1779pub use utils::TimeGate;