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