From 3973e595b40148634dd191c893ab6018f4a6eda4 Mon Sep 17 00:00:00 2001 From: carrion256 Date: Thu, 18 Jun 2026 17:02:18 +0200 Subject: [PATCH 01/11] ENG-162 add Kani invariant coverage --- Cargo.toml | 3 + .../tests/universal_account.rs | 234 ++++++++++++- contract/vault/kernel/Cargo.toml | 3 + contract/vault/kernel/src/lib.rs | 331 ++++++++++++++++++ contract/vault/kernel/tests/property_tests.rs | 300 +++++++++++++++- fuzz/fuzz_targets/fuzz_fee_math.rs | 29 ++ .../src/controller/universal_account.rs | 4 + universal-account/src/authentication/mod.rs | 66 ++++ universal-account/src/execute_args.rs | 222 +++++++++++- universal-account/src/state/migration.rs | 61 ++++ 10 files changed, 1249 insertions(+), 4 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 82a73519a..a2ade5daa 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -202,6 +202,9 @@ doc_markdown = "allow" result_large_err = "allow" ignore_without_reason = "allow" +[workspace.lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } + [profile.dev] incremental = true diff --git a/contract/universal-account/tests/universal_account.rs b/contract/universal-account/tests/universal_account.rs index 8108ef119..b779cfc43 100644 --- a/contract/universal-account/tests/universal_account.rs +++ b/contract/universal-account/tests/universal_account.rs @@ -12,7 +12,7 @@ use templar_universal_account::{ authentication::{with_raw_string::WithRawString, Payload}, state, transaction::{FunctionCallAction, Transaction}, - KeyParameters, PayloadExecutionParameters, NEAR_TESTNET_CHAIN_ID, + ExecuteArgs, KeyParameters, PayloadExecutionParameters, NEAR_TESTNET_CHAIN_ID, }; use test_utils::{ assert_all_outcomes_success, @@ -144,6 +144,24 @@ async fn setup( } } +fn signed_mint_execute_args( + sk: &TestSigner, + ft: &FtController, + parameters: PayloadExecutionParameters, + amount: u128, +) -> ExecuteArgs> { + let payload = WithRawString::from_parsed(Payload::new( + parameters, + vec![Transaction { + receiver_id: ft.contract().id().clone(), + actions: vec![mint(amount).into()].into(), + }] + .into(), + )); + + sk.execute_args(payload) +} + #[rstest] #[tokio::test] pub async fn universal_account( @@ -420,3 +438,217 @@ async fn reuse_nonce( uac.execute(&third_party, execute_args).await; } + +#[tokio::test] +async fn failed_execute_does_not_consume_nonce_and_success_consumes_once() { + let worker = worker().await; + let sk = TestSigner::random_passkey(); + let Setup { + uac, + ft, + third_party, + } = setup(&worker, &sk, false, ExecuteOnCreate::None).await; + + let key_entry = uac.get_key(sk.id()).await.unwrap(); + assert_eq!(key_entry.nonce.0, 0); + + let mut skipped_nonce = key_entry.clone(); + skipped_nonce.nonce = U64(2); + let execute_args = signed_mint_execute_args(&sk, &ft, skipped_nonce, 100); + + let result = third_party + .call(uac.contract().id(), "execute") + .args_json(json!({ "args": execute_args })) + .gas(near_sdk::Gas::from_tgas(300)) + .transact() + .await + .unwrap(); + assert!( + result.is_failure(), + "skipped nonce execution should fail: {:?}", + result.failures(), + ); + + let key_entry_after_failure = uac.get_key(sk.id()).await.unwrap(); + assert_eq!( + key_entry_after_failure.nonce.0, 0, + "failed verification must roll back the pre-verification nonce increment", + ); + let balance = ft.ft_balance_of(uac.contract.id()).await; + assert_eq!(balance.0, 0, "failed execution should not mint"); + + let execute_args = + signed_mint_execute_args(&sk, &ft, key_entry_after_failure.next_nonce(), 100); + let result = uac.execute(&third_party, execute_args).await; + assert_all_outcomes_success(&result); + + let key_entry_after_success = uac.get_key(sk.id()).await.unwrap(); + assert_eq!( + key_entry_after_success.nonce.0, 1, + "successful execution must consume exactly one nonce", + ); + let balance = ft.ft_balance_of(uac.contract.id()).await; + assert_eq!(balance.0, 100, "successful execution should mint once"); +} + +#[tokio::test] +async fn replayed_nonce_fails_without_reexecuting_payload() { + let worker = worker().await; + let sk = TestSigner::random_passkey(); + let Setup { + uac, + ft, + third_party, + } = setup(&worker, &sk, false, ExecuteOnCreate::None).await; + + let key_entry = uac.get_key(sk.id()).await.unwrap(); + let execute_args = signed_mint_execute_args(&sk, &ft, key_entry.next_nonce(), 100); + + let result = uac.execute(&third_party, execute_args.clone()).await; + assert_all_outcomes_success(&result); + + let key_entry_after_success = uac.get_key(sk.id()).await.unwrap(); + assert_eq!( + key_entry_after_success.nonce.0, 1, + "successful execution must consume the signed nonce", + ); + let balance = ft.ft_balance_of(uac.contract.id()).await; + assert_eq!(balance.0, 100, "payload should execute once"); + + let result = third_party + .call(uac.contract().id(), "execute") + .args_json(json!({ "args": execute_args })) + .gas(near_sdk::Gas::from_tgas(300)) + .transact() + .await + .unwrap(); + assert!( + result.is_failure(), + "replayed nonce execution should fail: {:?}", + result.failures(), + ); + + let key_entry_after_replay = uac.get_key(sk.id()).await.unwrap(); + assert_eq!( + key_entry_after_replay.nonce.0, 1, + "failed replay must not advance the nonce", + ); + let balance = ft.ft_balance_of(uac.contract.id()).await; + assert_eq!(balance.0, 100, "replayed payload must not execute again"); +} + +#[tokio::test] +async fn key_indexes_are_unique_across_remove_and_readd() { + let worker = worker().await; + let sk1 = TestSigner::random_passkey(); + let sk2 = TestSigner::random_ed25519_raw(); + let Setup { uac, .. } = setup(&worker, &sk1, false, ExecuteOnCreate::None).await; + + let key1 = sk1.id(); + let key2 = sk2.id(); + + let initial_entry = uac.get_key(key1.clone()).await.unwrap(); + assert_eq!(initial_entry.index.0, 0); + + let result = uac.add_key(uac.contract().as_account(), key2.clone()).await; + assert_all_outcomes_success(&result); + let second_entry = uac.get_key(key2.clone()).await.unwrap(); + assert_eq!(second_entry.index.0, 1); + + let result = uac + .remove_key(uac.contract().as_account(), key1.clone()) + .await; + assert_all_outcomes_success(&result); + assert!(uac.get_key(key1.clone()).await.is_none()); + + let result = uac.add_key(uac.contract().as_account(), key1.clone()).await; + assert_all_outcomes_success(&result); + let readded_entry = uac.get_key(key1.clone()).await.unwrap(); + assert_eq!( + readded_entry.index.0, 2, + "re-added keys must receive a fresh monotonic index", + ); + assert_eq!(readded_entry.nonce.0, 0); + + let keys = uac.list_keys(None, None).await; + assert_eq!(keys.len(), 2); + assert!(keys.contains(&key1)); + assert!(keys.contains(&key2)); +} + +#[tokio::test] +async fn cannot_remove_last_key() { + let worker = worker().await; + let sk = TestSigner::random_passkey(); + let Setup { uac, .. } = setup(&worker, &sk, false, ExecuteOnCreate::None).await; + + let result = uac + .contract() + .as_account() + .call(uac.contract().id(), "remove_key") + .args_json(json!({ "key": sk.id() })) + .gas(near_sdk::Gas::from_tgas(30)) + .transact() + .await + .unwrap(); + assert!( + result.is_failure(), + "last-key removal should fail: {:?}", + result.failures(), + ); + + let keys = uac.list_keys(None, None).await; + assert_eq!(keys, vec![sk.id()]); + assert!(uac.get_key(sk.id()).await.is_some()); +} + +#[tokio::test] +async fn removed_key_cannot_execute_transaction() { + let worker = worker().await; + let removed_sk = TestSigner::random_passkey(); + let retained_sk = TestSigner::random_ed25519_raw(); + let Setup { + uac, + ft, + third_party, + } = setup(&worker, &removed_sk, false, ExecuteOnCreate::None).await; + + let removed_key = removed_sk.id(); + let retained_key = retained_sk.id(); + + let result = uac + .add_key(uac.contract().as_account(), retained_key.clone()) + .await; + assert_all_outcomes_success(&result); + + let removed_entry_before = uac.get_key(removed_key.clone()).await.unwrap(); + let result = uac + .remove_key(uac.contract().as_account(), removed_key.clone()) + .await; + assert_all_outcomes_success(&result); + assert!(uac.get_key(removed_key.clone()).await.is_none()); + + let execute_args = + signed_mint_execute_args(&removed_sk, &ft, removed_entry_before.next_nonce(), 100); + let result = third_party + .call(uac.contract().id(), "execute") + .args_json(json!({ "args": execute_args })) + .gas(near_sdk::Gas::from_tgas(300)) + .transact() + .await + .unwrap(); + assert!( + result.is_failure(), + "removed key execution should fail: {:?}", + result.failures(), + ); + + assert!(uac.get_key(removed_key).await.is_none()); + let retained_entry = uac.get_key(retained_key).await.unwrap(); + assert_eq!( + retained_entry.nonce.0, 0, + "failed removed-key execution must not affect retained key state", + ); + let balance = ft.ft_balance_of(uac.contract.id()).await; + assert_eq!(balance.0, 0, "removed key payload must not execute"); +} diff --git a/contract/vault/kernel/Cargo.toml b/contract/vault/kernel/Cargo.toml index 256709f3f..539a6eac0 100644 --- a/contract/vault/kernel/Cargo.toml +++ b/contract/vault/kernel/Cargo.toml @@ -62,3 +62,6 @@ serde_json.workspace = true # Enable all action handlers for integration tests. # The `test` cfg only applies to unit tests in src/, not integration tests in tests/. templar-vault-kernel = { path = ".", features = ["all-actions"] } + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/contract/vault/kernel/src/lib.rs b/contract/vault/kernel/src/lib.rs index 51f40642d..0852cf774 100644 --- a/contract/vault/kernel/src/lib.rs +++ b/contract/vault/kernel/src/lib.rs @@ -60,5 +60,336 @@ pub use transitions::{ withdrawal_collected, withdrawal_settled, withdrawal_step_callback, TransitionError, TransitionRes, TransitionResult, WithdrawalRequest, }; + +#[cfg(kani)] +mod kani_proofs { + #[cfg(feature = "action-sync-external")] + use alloc::vec::Vec; + + use super::*; + + const MAX_AMOUNT: u128 = 32; + const OWNER: Address = Address([0x11; 32]); + const RECEIVER: Address = Address([0x22; 32]); + #[cfg(feature = "action-sync-external")] + const SELF: Address = Address([0x33; 32]); + + fn bounded_amount() -> u128 { + let amount = kani::any::(); + kani::assume(amount <= MAX_AMOUNT); + amount + } + + fn nonzero_bounded_amount() -> u128 { + let amount = bounded_amount(); + kani::assume(amount > 0); + amount + } + + #[cfg(feature = "action-sync-external")] + fn zero_fee_config() -> VaultConfig { + VaultConfig { + fees: FeesSpec::zero(), + min_withdrawal_assets: 0, + withdrawal_cooldown_ns: 0, + max_pending_withdrawals: 3, + paused: false, + virtual_shares: 0, + virtual_assets: 0, + } + } + + #[kani::proof] + fn bounded_initial_state_preserves_total_asset_invariant() { + let idle = bounded_amount(); + let external = bounded_amount(); + let shares = bounded_amount(); + + let state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + + assert!(state.check_invariant()); + assert_eq!( + state.total_assets, + state.idle_assets + state.external_assets + ); + assert_eq!(state.total_shares, shares); + assert_eq!(state.withdraw_queue.status().length, 0); + } + + #[kani::proof] + fn restore_to_idle_preserves_total_asset_invariant() { + let idle = bounded_amount(); + let external = bounded_amount(); + let restored = bounded_amount(); + let shares = bounded_amount(); + + let mut state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + state.restore_to_idle(restored); + + assert!(state.check_invariant()); + assert_eq!(state.idle_assets, idle + restored); + assert_eq!(state.external_assets, external); + assert_eq!(state.total_assets, idle + external + restored); + } + + #[kani::proof] + fn withdrawal_queue_enqueue_preserves_cached_escrow_and_claimability() { + let shares = nonzero_bounded_amount(); + let expected_assets = bounded_amount(); + let mut queue = WithdrawQueue::new(); + + let id = queue + .enqueue( + OWNER, + RECEIVER, + shares, + expected_assets, + TimestampNs::ZERO, + 3, + ) + .unwrap(); + + let status = queue.status(); + assert_eq!(id, 0); + assert!(queue.check_invariants_with_max(3)); + assert_eq!(status.length, 1); + assert_eq!(status.total_escrow_shares, shares); + assert_eq!(status.total_expected_assets, expected_assets); + assert!(queue.contains(id)); + assert!(queue.head().is_some()); + } + + #[kani::proof] + #[kani::unwind(8)] + fn two_entry_withdrawal_queue_preserves_cached_escrow_and_claimability() { + let first_shares = nonzero_bounded_amount(); + let second_shares = nonzero_bounded_amount(); + let first_expected_assets = bounded_amount(); + let second_expected_assets = bounded_amount(); + let mut queue = WithdrawQueue::new(); + + let first_id = queue + .enqueue( + OWNER, + RECEIVER, + first_shares, + first_expected_assets, + TimestampNs::ZERO, + 3, + ) + .unwrap(); + let second_id = queue + .enqueue( + RECEIVER, + OWNER, + second_shares, + second_expected_assets, + TimestampNs::ZERO, + 3, + ) + .unwrap(); + + let status = queue.status(); + let first = queue + .get(first_id) + .expect("first withdrawal should be queued"); + let second = queue + .get(second_id) + .expect("second withdrawal should be queued"); + + assert_eq!(first_id, 0); + assert_eq!(second_id, 1); + assert!(queue.check_invariants_with_max(3)); + assert_eq!(status.length, 2); + assert_eq!(status.total_escrow_shares, first_shares + second_shares); + assert_eq!( + status.total_expected_assets, + first_expected_assets + second_expected_assets + ); + assert!(queue.contains(first_id)); + assert!(queue.contains(second_id)); + assert_eq!(queue.head().map(|(id, _)| id), Some(first_id)); + assert_eq!(first.escrow_shares, first_shares); + assert_eq!(first.expected_assets, first_expected_assets); + assert_eq!(second.escrow_shares, second_shares); + assert_eq!(second.expected_assets, second_expected_assets); + } + + #[kani::proof] + #[kani::unwind(8)] + fn two_entry_withdrawal_queue_dequeues_fifo_and_preserves_cache() { + let first_shares = nonzero_bounded_amount(); + let second_shares = nonzero_bounded_amount(); + let first_expected_assets = bounded_amount(); + let second_expected_assets = bounded_amount(); + let mut queue = WithdrawQueue::new(); + + let first_id = queue + .enqueue( + OWNER, + RECEIVER, + first_shares, + first_expected_assets, + TimestampNs::ZERO, + 3, + ) + .unwrap(); + let second_id = queue + .enqueue( + RECEIVER, + OWNER, + second_shares, + second_expected_assets, + TimestampNs::ZERO, + 3, + ) + .unwrap(); + + let (dequeued_id, dequeued) = queue.dequeue().expect("first withdrawal should dequeue"); + let status = queue.status(); + + assert_eq!(dequeued_id, first_id); + assert_eq!(dequeued.escrow_shares, first_shares); + assert_eq!(dequeued.expected_assets, first_expected_assets); + assert!(queue.check_invariants_with_max(3)); + assert_eq!(status.length, 1); + assert_eq!(status.total_escrow_shares, second_shares); + assert_eq!(status.total_expected_assets, second_expected_assets); + assert!(!queue.contains(first_id)); + assert!(queue.contains(second_id)); + assert_eq!(queue.head().map(|(id, _)| id), Some(second_id)); + } + + #[cfg(feature = "action-sync-external")] + #[kani::proof] + fn rebalance_withdraw_conserves_total_assets_and_moves_external_to_idle() { + let idle = bounded_amount(); + let external = bounded_amount(); + let shares = bounded_amount(); + let amount = bounded_amount(); + kani::assume(amount <= external); + + let state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + let before_total_assets = state.total_assets; + let before_total_shares = state.total_shares; + + let result = match apply_action( + state, + &zero_fee_config(), + None, + &SELF, + KernelAction::rebalance_withdraw(0, amount, TimestampNs::ZERO), + ) { + Ok(result) => result, + Err(_) => panic!("bounded rebalance withdraw should succeed"), + }; + + assert_eq!( + result.state.total_assets, + result.state.idle_assets + result.state.external_assets + ); + assert_eq!(result.state.total_assets, before_total_assets); + assert_eq!(result.state.total_shares, before_total_shares); + assert_eq!(result.state.idle_assets, idle + amount); + assert_eq!(result.state.external_assets, external - amount); + } + + #[cfg(feature = "action-sync-external")] + #[kani::proof] + fn sync_external_assets_preserves_total_as_idle_plus_external() { + let idle = bounded_amount(); + let external = bounded_amount(); + let synced_external = bounded_amount(); + let shares = bounded_amount(); + let op_id = 7; + + let mut state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + state.op_state = OpState::Allocating(AllocatingState { + op_id, + index: 0, + remaining: 0, + plan: Vec::new(), + }); + + let result = match apply_action( + state, + &zero_fee_config(), + None, + &SELF, + KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO), + ) { + Ok(result) => result, + Err(_) => panic!("bounded sync external assets should succeed"), + }; + + assert_eq!( + result.state.total_assets, + result.state.idle_assets + result.state.external_assets + ); + assert_eq!(result.state.idle_assets, idle); + assert_eq!(result.state.external_assets, synced_external); + assert_eq!(result.state.total_assets, idle + synced_external); + assert_eq!(result.state.total_shares, shares); + } + + #[cfg(feature = "action-sync-external")] + #[kani::proof] + fn bounded_sync_then_rebalance_conserves_accounting_across_actions() { + let idle = bounded_amount(); + let external = bounded_amount(); + let shares = bounded_amount(); + let synced_external = bounded_amount(); + let rebalance_amount = bounded_amount(); + let op_id = 9; + kani::assume(rebalance_amount <= synced_external); + + let mut state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + state.op_state = OpState::Allocating(AllocatingState { + op_id, + index: 0, + remaining: 0, + plan: Vec::new(), + }); + + let synced = match apply_action( + state, + &zero_fee_config(), + None, + &SELF, + KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO), + ) { + Ok(result) => result.state, + Err(_) => panic!("bounded sync external assets should succeed"), + }; + + let rebalanced = match apply_action( + synced, + &zero_fee_config(), + None, + &SELF, + KernelAction::rebalance_withdraw(op_id, rebalance_amount, TimestampNs::ZERO), + ) { + Ok(result) => result.state, + Err(_) => panic!("bounded rebalance withdraw should succeed after sync"), + }; + + assert_eq!( + rebalanced.total_assets, + rebalanced.idle_assets + rebalanced.external_assets + ); + assert_eq!(rebalanced.total_shares, shares); + assert_eq!(rebalanced.idle_assets, idle + rebalance_amount); + assert_eq!( + rebalanced.external_assets, + synced_external - rebalance_amount + ); + assert_eq!(rebalanced.total_assets, idle + synced_external); + } +} pub use types::{ActualIdx, Address, AssetId, DurationNs, ExpectedIdx, KernelVersion, TimestampNs}; pub use utils::TimeGate; diff --git a/contract/vault/kernel/tests/property_tests.rs b/contract/vault/kernel/tests/property_tests.rs index 29cc91088..82da114e8 100644 --- a/contract/vault/kernel/tests/property_tests.rs +++ b/contract/vault/kernel/tests/property_tests.rs @@ -1505,7 +1505,7 @@ proptest! { // Deterministic Boundary / Edge Case Tests use templar_vault_kernel::{ - preview_deposit_shares, preview_withdraw_assets, PayoutOutcome, VaultConfig, + convert_to_assets, preview_deposit_shares, preview_withdraw_assets, PayoutOutcome, VaultConfig, }; fn default_config() -> VaultConfig { @@ -1532,6 +1532,253 @@ fn self_addr() -> templar_vault_kernel::Address { templar_vault_kernel::Address([99u8; 32]) } +proptest! { + #[test] + fn prop_asset_share_mutations_do_not_overflow_or_underflow( + idle in any::(), + total_shares in any::(), + assets_in in any::(), + ) { + let mut state = default_state(); + state.total_assets = idle; + state.idle_assets = idle; + state.total_shares = total_shares; + state.fee_anchor = FeeAccrualAnchor::new(idle, TimestampNs(0)); + let old_state = state.clone(); + let config = default_config(); + + let result = apply_action( + state, + &config, + None, + &self_addr(), + KernelAction::Deposit { + owner: owner_addr(1), + receiver: receiver_addr(1), + assets_in, + min_shares_out: 0, + now_ns: TimestampNs(1), + }, + ); + + if let Ok(result) = result { + prop_assert_eq!( + result.state.total_assets.checked_sub(old_state.total_assets), + Some(assets_in), + ); + prop_assert_eq!( + result.state.idle_assets.checked_sub(old_state.idle_assets), + Some(assets_in), + ); + prop_assert!(result.state.total_shares >= old_state.total_shares); + prop_assert!(result.state.check_invariant()); + } + } + + #[test] + fn prop_atomic_withdraw_respects_idle_cap( + idle in 1u128..=1_000_000_000_000u128, + external in 0u128..=1_000_000_000_000u128, + total_shares in 1u128..=1_000_000_000_000u128, + assets_out in 1u128..=2_000_000_000_000u128, + ) { + let mut state = default_state(); + state.total_assets = idle + external; + state.idle_assets = idle; + state.external_assets = external; + state.total_shares = total_shares; + state.fee_anchor = FeeAccrualAnchor::new(state.total_assets, TimestampNs(0)); + let old_state = state.clone(); + let config = default_config(); + let owner = owner_addr(1); + let receiver = receiver_addr(1); + + let result = apply_action( + state, + &config, + None, + &self_addr(), + KernelAction::AtomicWithdraw { + owner, + receiver, + operator: owner, + assets_out, + max_shares_burned: u128::MAX, + now_ns: TimestampNs(1), + }, + ); + + if assets_out > old_state.idle_assets { + prop_assert!(result.is_err(), "atomic withdraw over idle cap succeeded"); + return Ok(()); + } + + if let Ok(result) = result { + let burned_shares = result + .effects + .iter() + .find_map(|effect| match effect { + KernelEffect::BurnShares { owner: effect_owner, shares } + if *effect_owner == owner => Some(*shares), + _ => None, + }) + .expect("successful atomic withdraw must burn shares"); + let transferred_assets = result + .effects + .iter() + .find_map(|effect| match effect { + KernelEffect::TransferAssets { to, amount } if *to == receiver => Some(*amount), + _ => None, + }) + .expect("successful atomic withdraw must transfer assets"); + + prop_assert_eq!(transferred_assets, assets_out); + prop_assert!(burned_shares <= old_state.total_shares); + prop_assert_eq!(result.state.idle_assets, old_state.idle_assets - assets_out); + prop_assert_eq!(result.state.total_assets, old_state.total_assets - assets_out); + prop_assert_eq!( + result.state.total_shares, + old_state.total_shares - burned_shares, + ); + prop_assert!(result.state.check_invariant()); + } + } + + #[test] + fn prop_atomic_redeem_respects_idle_cap( + idle in 1u128..=1_000_000_000_000u128, + external in 0u128..=1_000_000_000_000u128, + total_shares in 1u128..=1_000_000_000_000u128, + shares in 1u128..=2_000_000_000_000u128, + ) { + let mut state = default_state(); + state.total_assets = idle + external; + state.idle_assets = idle; + state.external_assets = external; + state.total_shares = total_shares; + state.fee_anchor = FeeAccrualAnchor::new(state.total_assets, TimestampNs(0)); + let old_state = state.clone(); + let config = default_config(); + let owner = owner_addr(1); + let receiver = receiver_addr(1); + let previewed_assets = preview_withdraw_assets(&old_state, &config, shares); + + let result = apply_action( + state, + &config, + None, + &self_addr(), + KernelAction::AtomicRedeem { + owner, + receiver, + operator: owner, + shares, + min_assets_out: 0, + now_ns: TimestampNs(1), + }, + ); + + if let Ok(result) = result { + let burned_shares = result + .effects + .iter() + .find_map(|effect| match effect { + KernelEffect::BurnShares { owner: effect_owner, shares } + if *effect_owner == owner => Some(*shares), + _ => None, + }) + .expect("successful atomic redeem must burn shares"); + let transferred_assets = result + .effects + .iter() + .find_map(|effect| match effect { + KernelEffect::TransferAssets { to, amount } if *to == receiver => Some(*amount), + _ => None, + }) + .expect("successful atomic redeem must transfer assets"); + + prop_assert_eq!(burned_shares, shares); + prop_assert_eq!(transferred_assets, previewed_assets); + prop_assert!(burned_shares <= old_state.total_shares); + prop_assert!(transferred_assets <= old_state.idle_assets); + prop_assert_eq!(result.state.idle_assets, old_state.idle_assets - transferred_assets); + prop_assert_eq!(result.state.total_assets, old_state.total_assets - transferred_assets); + prop_assert_eq!( + result.state.total_shares, + old_state.total_shares - burned_shares, + ); + prop_assert!(result.state.check_invariant()); + } + } + + #[test] + fn prop_request_withdraw_escrow_conservation( + idle in 1u128..=1_000_000_000_000u128, + external in 0u128..=1_000_000_000_000u128, + total_shares in 1u128..=1_000_000_000_000u128, + requested_shares in 1u128..=1_000_000_000_000u128, + ) { + let mut config = default_config(); + config.min_withdrawal_assets = 0; + + let mut state = default_state(); + state.total_assets = idle + external; + state.idle_assets = idle; + state.external_assets = external; + state.total_shares = total_shares; + state.fee_anchor = FeeAccrualAnchor::new(state.total_assets, TimestampNs(0)); + let shares = requested_shares.min(total_shares); + let expected_assets = convert_to_assets(&state, &config, shares); + let old_state = state.clone(); + let owner = owner_addr(1); + let receiver = receiver_addr(1); + let vault = self_addr(); + + let result = apply_action( + state, + &config, + None, + &vault, + KernelAction::RequestWithdraw { + owner, + receiver, + shares, + min_assets_out: 0, + now_ns: TimestampNs(1), + }, + ) + .expect("valid request withdraw should enqueue"); + + prop_assert_eq!(result.state.total_assets, old_state.total_assets); + prop_assert_eq!(result.state.idle_assets, old_state.idle_assets); + prop_assert_eq!(result.state.external_assets, old_state.external_assets); + prop_assert_eq!(result.state.total_shares, old_state.total_shares); + prop_assert!(expected_assets <= old_state.total_assets); + prop_assert!(result.state.check_invariant()); + + let pending = result + .state + .withdraw_queue + .pending_withdrawals() + .values() + .next() + .expect("request should be queued"); + prop_assert_eq!(pending.escrow_shares, shares); + prop_assert_eq!(pending.expected_assets, expected_assets); + + let transfer = result + .effects + .iter() + .find_map(|effect| match effect { + KernelEffect::TransferShares { from, to, shares: effect_shares } + if *from == owner && *to == vault => Some(*effect_shares), + _ => None, + }) + .expect("request withdraw must escrow shares"); + prop_assert_eq!(transfer, shares); + } +} + /// Boundary 1: Depositing zero assets returns ZeroAmount error. #[test] fn deposit_zero_assets_returns_zero_amount() { @@ -3706,6 +3953,57 @@ proptest! { } } + /// Parity property: successful deposits mint exactly the previewed shares. + #[test] + fn prop_deposit_mints_previewed_shares( + assets in 1u128..=1_000_000_000u128, + initial_idle in 0u128..=1_000_000_000u128, + initial_shares in 0u128..=1_000_000_000u128, + ) { + let config = default_config(); + let state = VaultState::with_initial( + initial_idle, + initial_shares, + initial_idle, + 0, + TimestampNs(0), + ); + let previewed_shares = preview_deposit_shares(&state, &config, assets); + if previewed_shares == 0 { + return Ok(()); + } + + let result = apply_action( + state, + &config, + None, + &self_addr(), + KernelAction::Deposit { + owner: owner_addr(1), + receiver: receiver_addr(1), + assets_in: assets, + min_shares_out: previewed_shares, + now_ns: TimestampNs(1), + }, + ); + prop_assert!(result.is_ok(), "deposit with previewed minimum should succeed"); + let result = result.expect("result was checked as ok"); + + let minted_shares = result + .effects + .iter() + .find_map(|effect| match effect { + KernelEffect::MintShares { owner, shares } if *owner == receiver_addr(1) => { + Some(*shares) + } + _ => None, + }) + .expect("successful deposit must mint shares"); + + prop_assert_eq!(minted_shares, previewed_shares); + prop_assert!(result.state.check_invariant()); + } + /// Parity property: executor idle_assets decrement + kernel abort always /// restores to original value. #[test] diff --git a/fuzz/fuzz_targets/fuzz_fee_math.rs b/fuzz/fuzz_targets/fuzz_fee_math.rs index a69610d82..53bf79f5e 100644 --- a/fuzz/fuzz_targets/fuzz_fee_math.rs +++ b/fuzz/fuzz_targets/fuzz_fee_math.rs @@ -125,6 +125,35 @@ fuzz_target!(|input: FeeMathInput| { let amount = input.convert_amount; let cap = input.convert_cap; let err = InvalidStateCode::Unknown; + let max_cap = u128::MAX; + + if let (Ok(floor), Ok(ceil)) = ( + convert_to_shares_bounded(&state, &config, amount, max_cap, err), + convert_to_shares_ceil_bounded(&state, &config, amount, max_cap, err), + ) { + assert!( + floor <= ceil, + "convert_to_shares floor ({floor}) exceeded ceil ({ceil})", + ); + assert!( + ceil <= floor.saturating_add(1), + "convert_to_shares ceil ({ceil}) was more than floor + 1 ({floor})", + ); + } + + if let (Ok(floor), Ok(ceil)) = ( + convert_to_assets_bounded(&state, &config, amount, max_cap, err), + convert_to_assets_ceil_bounded(&state, &config, amount, max_cap, err), + ) { + assert!( + floor <= ceil, + "convert_to_assets floor ({floor}) exceeded ceil ({ceil})", + ); + assert!( + ceil <= floor.saturating_add(1), + "convert_to_assets ceil ({ceil}) was more than floor + 1 ({floor})", + ); + } if let Ok(v) = convert_to_shares_bounded(&state, &config, amount, cap, err) { assert!(v <= cap, "shares: bounded result exceeded cap"); diff --git a/test-utils/src/controller/universal_account.rs b/test-utils/src/controller/universal_account.rs index faf6543c2..08b01dfcb 100644 --- a/test-utils/src/controller/universal_account.rs +++ b/test-utils/src/controller/universal_account.rs @@ -72,6 +72,10 @@ impl UniversalAccountController { #[view] pub fn list_keys(offset: Option, count: Option) -> Vec; + #[call(exec, tgas(30))] + pub fn add_key(key: KeyId); + #[call(exec, tgas(30))] + pub fn remove_key(key: KeyId); #[call(exec, tgas(300))] pub fn execute(args: ExecuteArgs>); } diff --git a/universal-account/src/authentication/mod.rs b/universal-account/src/authentication/mod.rs index 19432cc67..8d6b8569a 100644 --- a/universal-account/src/authentication/mod.rs +++ b/universal-account/src/authentication/mod.rs @@ -202,3 +202,69 @@ pub trait HashForSigning { near_sdk::env::sha256_array(self.preimage_for_signing()) } } + +#[cfg(kani)] +mod kani_proofs { + use near_sdk::{json_types::U64, AccountId}; + + use crate::{ + authentication::{ed25519::raw, with_raw_string::WithRawString}, + encoding, PayloadExecutionParameters, + }; + + use super::*; + + // These proofs start from a message whose signature has already been accepted. + // They prove execution-parameter and payload plumbing, not cryptographic binding. + fn account_id() -> AccountId { + "account.near".parse().unwrap() + } + + fn execution_parameters() -> PayloadExecutionParameters { + PayloadExecutionParameters::builder_empty() + .block_height(7_u64) + .index(3_u64) + .nonce(11_u64) + .verifying_contract(account_id()) + .build() + } + + fn valid_raw_message(payload: u8) -> MessageWithValidSignature> { + let message = raw::Message::new(WithRawString { + raw: String::new(), + parsed: Payload::new(execution_parameters(), payload), + }); + + MessageWithValidSignature(MessageWithSignature { + message, + signature: encoding::ed25519::Signature([0u8; 64]), + auxiliary: (), + }) + } + + #[kani::proof] + fn valid_message_execution_returns_exact_signed_payload() { + let signed_payload = kani::any::(); + + let returned = valid_raw_message(signed_payload) + .verify_execution(&execution_parameters(), |_| true) + .unwrap(); + + assert_eq!(returned, signed_payload); + } + + #[kani::proof] + fn valid_message_execution_rejects_parameter_mismatch_before_payload_return() { + let signed_payload = kani::any::(); + let mut expected_parameters = execution_parameters(); + expected_parameters.nonce = U64(expected_parameters.nonce.0 + 1); + + let result = + valid_raw_message(signed_payload).verify_execution(&expected_parameters, |_| true); + + assert!(matches!( + result, + Err(ExecutionError::Mismatch { field: "nonce", .. }) + )); + } +} diff --git a/universal-account/src/execute_args.rs b/universal-account/src/execute_args.rs index 1d1a88444..c9ff2524f 100644 --- a/universal-account/src/execute_args.rs +++ b/universal-account/src/execute_args.rs @@ -162,10 +162,11 @@ mod tests { authentication::{ ed25519::raw, passkey::data::{AuthenticatorData, ClientDataJson}, + with_raw_string::WithRawString, HashForSigning, Payload, }, - transaction::{self, Transaction}, - KeyParameters, NEAR_TESTNET_CHAIN_ID, + transaction::{self, Action, Transaction}, + KeyParameters, NEAR_MAINNET_CHAIN_ID, NEAR_TESTNET_CHAIN_ID, }; use super::*; @@ -278,6 +279,40 @@ mod tests { .into() } + #[test] + #[ignore = "ENG-162: enable after PayloadExecutionParameters stores and verifies immutable domain_id"] + fn verify_rejects_same_chain_and_contract_with_different_domain_id() { + let signed_domain_id = [1u8; 32]; + let verifier_domain_id = [2u8; 32]; + assert_ne!(signed_domain_id, verifier_domain_id); + + let expected_parameters = PayloadExecutionParameters::builder(NEAR_TESTNET_CHAIN_ID) + .with_key_parameters(KeyParameters { + block_height: U64(12345), + index: U64(1), + nonce: U64(44), + }) + .verifying_contract(AccountId::from_str("my-universal-account.near").unwrap()) + .build_salt(); + + let error = passkey_execute_args() + .verify(&expected_parameters, |_| true) + .expect_err( + "same chain_id and verifying_contract must still reject a different domain_id", + ); + + assert!( + matches!( + error, + VerificationError::Execution(ExecutionError::Mismatch { + field: "domain_id", + .. + }) + ), + "expected domain_id mismatch, got {error:?}", + ); + } + #[rstest] #[case("my-universal-account.near", 12345, 1, 44)] #[should_panic = r#"Execution(Mismatch { field: "verifying_contract", expected: "my-universal-account.nearx", actual: "my-universal-account.near" })"#] @@ -339,6 +374,189 @@ mod tests { .unwrap(); } + #[derive(Clone, Copy)] + enum DomainMutation { + BlockHeight, + ChainId, + Index, + Name, + Nonce, + Salt, + VerifyingContract, + Version, + } + + impl DomainMutation { + fn field(self) -> &'static str { + match self { + Self::BlockHeight => "block_height", + Self::ChainId => "chain_id", + Self::Index => "index", + Self::Name => "name", + Self::Nonce => "nonce", + Self::Salt => "salt", + Self::VerifyingContract => "verifying_contract", + Self::Version => "version", + } + } + + fn apply(self, parameters: &mut PayloadExecutionParameters) { + match self { + Self::BlockHeight => parameters.block_height = U64(parameters.block_height.0 + 1), + Self::ChainId => parameters.chain_id = Some(NEAR_MAINNET_CHAIN_ID.into()), + Self::Index => parameters.index = U64(parameters.index.0 + 1), + Self::Name => parameters.name = Some("Wrong Universal Account".to_string()), + Self::Nonce => parameters.nonce = U64(parameters.nonce.0 + 1), + Self::Salt => parameters.salt = Some([7u8; 32].into()), + Self::VerifyingContract => { + parameters.verifying_contract = + AccountId::from_str("other-universal-account.near").unwrap(); + } + Self::Version => parameters.version = Some("0.0.0".to_string()), + } + } + } + + #[rstest] + #[case::block_height(DomainMutation::BlockHeight)] + #[case::chain_id(DomainMutation::ChainId)] + #[case::index(DomainMutation::Index)] + #[case::name(DomainMutation::Name)] + #[case::nonce(DomainMutation::Nonce)] + #[case::salt(DomainMutation::Salt)] + #[case::verifying_contract(DomainMutation::VerifyingContract)] + #[case::version(DomainMutation::Version)] + #[test] + fn verify_rejects_each_execution_domain_mismatch(#[case] mutation: DomainMutation) { + let mut expected_parameters = PayloadExecutionParameters::builder(NEAR_TESTNET_CHAIN_ID) + .with_key_parameters(KeyParameters { + block_height: U64(12345), + index: U64(1), + nonce: U64(44), + }) + .verifying_contract(AccountId::from_str("my-universal-account.near").unwrap()) + .build_salt(); + mutation.apply(&mut expected_parameters); + + let error = passkey_execute_args() + .verify(&expected_parameters, |_| true) + .unwrap_err(); + + assert!( + matches!( + error, + VerificationError::Execution(ExecutionError::Mismatch { field, .. }) + if field == mutation.field() + ), + "expected {} mismatch, got {error:?}", + mutation.field(), + ); + } + + #[derive(Clone, Copy)] + enum SignedPayloadMutation { + Receiver, + FunctionName, + Arguments, + Amount, + Gas, + } + + impl SignedPayloadMutation { + fn apply(self, payload: &mut [Transaction]) { + let transaction = &mut payload[0]; + + match self { + Self::Receiver => { + transaction.receiver_id = AccountId::from_str("attacker.near").unwrap(); + } + Self::FunctionName => { + let Action::FunctionCall(call) = &mut transaction.actions[0] else { + panic!("test payload action must be a function call"); + }; + call.function_name = "ft_transfer_call".to_string(); + } + Self::Arguments => { + let Action::FunctionCall(call) = &mut transaction.actions[0] else { + panic!("test payload action must be a function call"); + }; + call.arguments = + br#"{"receiver_id":"attacker.near","amount":"100"}"#.to_vec().into(); + } + Self::Amount => { + let Action::FunctionCall(call) = &mut transaction.actions[0] else { + panic!("test payload action must be a function call"); + }; + call.amount = NearToken::from_yoctonear(2); + } + Self::Gas => { + let Action::FunctionCall(call) = &mut transaction.actions[0] else { + panic!("test payload action must be a function call"); + }; + call.gas = near_sdk::Gas::from_tgas(31); + } + } + } + + fn apply_to_execute_args(self, exec_args: &mut ExecuteArgs>) { + macro_rules! mutate_message { + ($args:ident) => {{ + let mut payload = $args.mws.message.0.parsed.clone(); + self.apply(payload.payload_mut()); + $args.mws.message.0 = WithRawString::from_parsed(payload); + }}; + } + + match exec_args { + ExecuteArgs::Passkey(args) => mutate_message!(args), + ExecuteArgs::Ed25519Raw(args) => mutate_message!(args), + ExecuteArgs::Eip712(args) => mutate_message!(args), + ExecuteArgs::Sep53(args) => mutate_message!(args), + ExecuteArgs::Eip191(args) => mutate_message!(args), + } + } + } + + #[rstest] + #[case::receiver(SignedPayloadMutation::Receiver)] + #[case::function_name(SignedPayloadMutation::FunctionName)] + #[case::arguments(SignedPayloadMutation::Arguments)] + #[case::amount(SignedPayloadMutation::Amount)] + #[case::gas(SignedPayloadMutation::Gas)] + #[test] + fn verify_rejects_signed_payload_mutation_for_each_format( + #[values( + passkey_execute_args(), + ed25519_raw_execute_args(), + eip712_execute_args(), + sep53_execute_args(), + eip191_execute_args() + )] + mut exec_args: ExecuteArgs>, + #[case] mutation: SignedPayloadMutation, + ) { + mutation.apply_to_execute_args(&mut exec_args); + + let error = exec_args + .verify( + &PayloadExecutionParameters::builder(NEAR_TESTNET_CHAIN_ID) + .with_key_parameters(KeyParameters { + block_height: U64(12345), + index: U64(1), + nonce: U64(44), + }) + .verifying_contract(AccountId::from_str("my-universal-account.near").unwrap()) + .build_salt(), + |_| true, + ) + .expect_err("signed payload mutation must invalidate the signature"); + + assert!( + matches!(error, VerificationError::Signature(_)), + "expected signature rejection, got {error:?}", + ); + } + #[rstest] #[case::ed25519raw_unflattened("e3ff9a0ab355.user0.tmplr.near", 173_342_352, 41, r#"{"Ed25519Raw":{"key":"ed25519:BTPUmzP1v4t7kNB69i4v8d1Ci5egN62Fs8QjePMSfJvo","message":{"message":"{\"parameters\":{\"block_height\":\"173342352\",\"index\":\"0\",\"nonce\":\"41\"},\"account_id\":\"e3ff9a0ab355.user0.tmplr.near\",\"payload\":[{\"receiver_id\":\"pyth-oracle.near\",\"actions\":[{\"FunctionCall\":{\"function_name\":\"update_price_feeds\",\"arguments\":\"eyJkYXRhIjoiNTA0ZTQxNTUwMTAwMDAwMDAzYjgwMTAwMDAwMDA0MGQwMDVkY2EyNzdhYjk1NjViMjI0ZDZkY2NjZjBlNGVlMDdhZDM1NDhhMDViMTAwNGNjY2ZmMWI4YTlmMWFiNWZmOWQ0YzYxMzdhNWZlYTYxYThlNTFhOTZhZGM1Yjg4MjU0MzE3YWEwZjM1MzJkN2ZmY2VkZGMwNWE1ZGUwZDlhNjRjMDAwMzM5MmU5MTk1NDVjM2Q1Y2JmYWVmOGUxNDkxMzlmY2JiMzQ3ZjI4YTU5ZDVhNWRhZTE3Y2VhNjFjMjFjNDU0N2I1NmY3MzQyNzVkMzAwNWQ1YTYyN2I3YTMwZmNlMjBmOTA5MjNjMjU3MWY4Yjk4MGUxYjVjNjQ4YjQ4Mjg0M2U0MDEwNGJhOTRmOWFiMzcxMjY3ODdlOTdlZmNkODlmMzU5OTdmYTc0NDI0N2FlNmQ5NTVlZGU3ZTVjNGFiNTE2ODA5N2YyZjNiMmM3ZTk1NmUzM2U3MzQzNDc3Mzk4YzhjNTZhN2U1YzM0MDFhZWFiNmY3ZDc4NmI1MWFmYzIzN2E5OGVhMDEwNjk4NTllMjMyNGFhNjM2YzI5NjU1YzJmOWQxMzgyZGExOTg4M2E2NWIyMzc1NWI4MzEzMmMzZDhhNDA4MjhiMDIxMTMzMTQxMmM0NzYxN2NlYWVkYTM3MTIxNjM2YmRkNjFjY2E2NzVkZWQwZTdmNjg1ZTc1OTJiYzY2OWIwNjI3MDAwODBmNzk1NTJhNjY4ZmM2YWEyMjVmNzkwODBjMmY1YzEzNmE2MDU1NjI3M2EwYzRjOWNlMTc2ODUzMDFiMGJlMTI1YWE2NTBjZDhlNzkxYTVhMGY0Yjg5ODdhZmZjNTFkMDdiMGYzNzcxMjAwMWUwNmI1MjRhYzkwMzI3Y2ZiMWFmMDAwYTczZTgxZjU1ODYwMGNiNGRkYTEwNTFjMWQ0MjBjNjQxNDgxNjVlZjM4MGVjNDU0ZDQwZjcwYTE4MTY5YWJmNzUyMWZkMzI4MWY5ZTM3YTRkMTM1YTU2Y2YwMDhjZDVkZGQ3ZmMzNTM2ZDU1M2QyODhlMmI0YjU5ZWRiMTA5NzVlMDAwYjEzYzI3YjA4Nzc5YTM4Nzk1ODdmMWVjMzNiNmU3YjVmNjgzY2I3NjRiOWM2YmVhNGEwMTExNmE4NjFjMjg1Yjc2MjhhMjUxMDk0NzI1YjFlOTY2Mjg3NThkYjg3YTg5MDY5OTQ5OTk4M2JiZTUxMmU2NGQxZjY2NTJkMDU1ZjQ0MDEwY2U3NWU3ZDFiNzRkZjFmMDRkYjZjZDhjNjU4Y2QwZmU5ODVjMjdkMjljYWM0OGU5MzI0ZDgxMGM5ZmZlYzJjMWEyYWQ2ZWYyYTRjNmRhZTMzMTIxYWY5NjUyZDJmYjk1YjZjN2FhZjA2MzQ3ZWE4OTU3ZDdhNzdhM2M5NGRjMTY3MDEwZDE3Yzk1NzBjZGZkOGI5Njc4ZjIyYTRlMGQzZDBmNWQ3ZTM1NzVmZjc1NzExODEyNTQzZDhlZWE3OWVjNzNkNWIzMmI0NTcwMDAwMDgyZjBiNTcwZmI4ZTRmMTFjOWE0ZTBiMmJkZGVlYmU0ZjQ4NDQxYzZjYWEyYzQ1ZDBmYTZmMDEwZTFkYjAyMWEzMzkyN2U1NmRlMGQ5OGJmMzZkMTUzNjEyMjM3N2NiNWU4NjQ3NzQ5NGJmMGYzZThhYWYyOWVhZTM3MGU2YmMzODc4ZWVmOTkxMjViMjk3NWU0OGY3MzhhYTg0MDNkOGEyZDhlMzFlNTMyMmY4NWNhZGFkZGMxMTEzMDAwZjFjZWIyYTBjZmU1ZTU0ZDRiYTIwMGRmY2Q2YzU3NmE3ZGViNzhkNGZiZTM5YTE4OWNlZDg1NDVjYWMzODYwMjg3MDE3NWQ1Y2M4YWZmNTRiMmNmNGRmZDUwYjc3YWFhMmRjZDk4YmVjZGEzODVlYWZhNGFhNjlkMzk1NDBiODJiMDAxMGVkNzBmNzY4OWQ1YTJkNzAxODJhZjVjMTAyYmZmZGI5ZGVmYzM2NDRiNzk0MGQ0ZmJmNDM4MzZiOWFkMzViZjM2ZGMwMTg0Y2Q4NTZjNDdmYWYzNWRlM2ZmYzg0YmExNzFkYWQxOWVmOTY2MTkxMDcyYWUxNmZlZmVhMzZiNmQ2MDAxMWJkY2RlOWExZWNmN2Q3ZjFlYjc3OTMzZDI5ZjA4MjFkNDE5NTFiZmFlYTA1YzEyZjc3ZmMyN2ZmNDA4YTA0NDc2ZGZiYmM0NWYwNWU3MmNiMGUwMzk4ZGIzOGMxZGM1OTZlY2IyMWJmNDhmN2I4NTU3MmE0N2Q5MjkyNzZlNGU1MDE2OTI5ODJkZjAwMDAwMDAwMDAxYWUxMDFmYWVkYWM1ODUxZTMyYjliMjNiNWY5NDExYThjMmJhYzRhYWUzZWQ0ZGQ3YjgxMWRkMWE3MmVhNGFhNzEwMDAwMDAwMDBhNGU0N2RlMDE0MTU1NTc1NjAwMDAwMDAwMDAwZjViZWViZjAwMDAyNzEwZTBiODlkNGFmNWYxMTA0MjJiZDUwMjM3ODdiYjFlMGE1MjMxODMxNDAyMDA1NTAwZWFhMDIwYzYxY2M0Nzk3MTI4MTM0NjFjZTE1Mzg5NGE5NmE2YzAwYjIxZWQwY2ZjMjc5OGQxZjlhOWU5Yzk0YTAwMDAwMDAwMDVmNTg5ZDYwMDAwMDAwMDAwMDEwNWQ1ZmZmZmZmZjgwMDAwMDAwMDY5Mjk4MmRmMDAwMDAwMDA2OTI5ODJkZjAwMDAwMDAwMDVmNThjOTIwMDAwMDAwMDAwMDExNjljMGRiOTVlZWM1NmYxMTkzNTZjY2YwZDdjNDg0ZmMyZTI0OTgzNTRjYjdmYzRjZTc2MTg5NzY0ZjJkMDNhODIwZTEwYmJhY2IwNzA0ZTJlNzAzNDYzNTE0NjVhZmY3Zjg2ZDQ1ZGUxY2FjMmQxYzhjMWEyMjk4NDljYTFkNjQ5ZmVjMGEwNWFiNDBmZTJjYzM0NWRkYjA2MGNmMjc0YjQ5ZmJlZmFjM2M1YjY5Njg2M2RlNzkwNDk2Nzc3NmRhMTRmYmFkMjJhODlhYjRmZGIyNzFmNzZjZWFjZjc2Y2M5MmQ0NDQ2NTgyZmE0NDU3NDlhZTliNTJhZWQxYTNiZWEzZjk4MWU4YjdkZmM0NjBjZDFlOWZlYmJjMWFjMDVjMjg0NzIzNGIwODZhY2U4MTRjZjQ0MTI0ZTM4OGExODllYTk0ODZjNTQ5N2ZkYzVjZTE4Y2Q0N2M4MDU5Njc4NTFiMTRhZDFjOGZkOWNmNTU0YjM5MjNmN2RhYjY5MmNjMjhkNzA4YTA2MDAwNzYzZmQyOWQxNDJjYWFjOGUxM2YwNTZmNWNmMDJhMDZjYmRjOTM1MzAzZjJmNGFiZmNhMzQ5NmY3OWNkY2MwYjZkZWY3Y2QxMjc0YWJmNjQ2NWMzZjM1N2UxNGNlNDc4MTlhNDVmOTcyZTk1ZTI0ZjYxYWY0ZjUxZjFmMjg0ZDQwMDA1NTAwYmU5YjU5ZDE3OGYwZDZhOTdhYjRjMzQzYmZmMmFhNjljYWExZWFhZTNlOTA0OGE2NTc4OGM1MjliMTI1YmIyNDAwMDAwMDBiMmRjNGQ3NTgwMDAwMDAwMDAzMjQ1ZDYxZmZmZmZmZjgwMDAwMDAwMDY5Mjk4MmRmMDAwMDAwMDA2OTI5ODJkZjAwMDAwMDBiMjZlZDM4YTgwMDAwMDAwMDAyYzE4Yzg0MGRhNDc0MTlkMTEyYWI4ZmI5Mjc1YjU2YmVhYzcxODkzMDlhMmY0ZjhmOGY2NjBmZmQ0YjMwMTIyZjRmN2ZkNTgyNjJjNjRkMTEyM2UwNjZmZDZkM2Q3NzAxYWQ1MjZmNDA5ZTMzNjE2NGI3Y2ZkYWM2NWQwZDZmYThkNDQ2M2I0MjFmYWYwMTQ1MjlkOWRmNWI1NDkxNWJlOTlkNDMzY2JiMDJjMGI2MGY3NGQzYzJhMTNiN2EyODQyOGZhYzE1N2ZkNTU0MTg2MzBiN2ZkNjk2ZWRiNjJmMTNhZGYzNjI4MDNjODUyMTYyZDg4NTQ1MmRhNzJkNzg0MGViMzQ1NjVhZjQ0MGM1OWUwOGJiYTAyYzk1ZThkZjdhYzQ2ZjY1MDg5ODg1OWU5NzI2MTAxNjIyNzA3ZjgxNTkyNzU0ZGVkMWQwYjc3OTBkOWFmODYyNjc2ODEyY2U1YTIwZjgxNGM0ZjBmM2M3ZGMyNDhlYmVjNTNlN2RiOWE3OTFlZjQ3YTAzYTY3NWQyOWE5MGNmYzYxNDJjYWFjOGUxM2YwNTZmNWNmMDJhMDZjYmRjOTM1MzAzZjJmNGFiZmNhMzQ5NmY3OWNkY2MwYjZkZWY3Y2QxMjc0YWJmNjQ2NWMzZjM1N2UxNGNlNDc4MTlhNDVmOTcyZTk1ZTI0ZjYxYWY0ZjUxZjFmMjg0ZDQwIn0=\",\"amount\":\"155000000000000\",\"gas\":\"155000000000000\"}}]},{\"receiver_id\":\"intents.near\",\"actions\":[{\"FunctionCall\":{\"function_name\":\"mt_transfer_call\",\"arguments\":\"eyJyZWNlaXZlcl9pZCI6Iml6ZWMtaXNvbHVzZGMudGVtcGxhci1hbHBoYS5uZWFyIiwiYW1vdW50IjoiMTcyMTc2NyIsIm1zZyI6IlwiUmVwYXlcIiIsInRva2VuX2lkIjoibmVwMTQxOnNvbC01Y2UzYmYzYTMxYWYxOGJlNDBiYTMwZjcyMTEwMWI0MzQxNjkwMTg2Lm9tZnQubmVhciJ9\",\"amount\":\"1\",\"gas\":\"50000000000000\"}}]},{\"receiver_id\":\"izec-isolusdc.templar-alpha.near\",\"actions\":[{\"FunctionCall\":{\"function_name\":\"withdraw_collateral\",\"arguments\":\"eyJhbW91bnQiOiI3MDUwMDAifQ==\",\"amount\":\"0\",\"gas\":\"50000000000000\"}}]}]}","signature":"ed25519:4CrFbqgiHo3BUv2QoHX7XDcRJqZeVvJJ8fB4SCgpzqSBPwsEyNCFT3uEKbwudDp2tzjQy9xPAeud6iq2qU1Crfet"}}}"#)] #[case::ed25519raw_flattened("e3ff9a0ab355.user0.tmplr.near", 173_342_352, 41, r#"{"Ed25519Raw":{"key":"ed25519:BTPUmzP1v4t7kNB69i4v8d1Ci5egN62Fs8QjePMSfJvo","message":"{\"parameters\":{\"block_height\":\"173342352\",\"index\":\"0\",\"nonce\":\"41\"},\"account_id\":\"e3ff9a0ab355.user0.tmplr.near\",\"payload\":[{\"receiver_id\":\"pyth-oracle.near\",\"actions\":[{\"FunctionCall\":{\"function_name\":\"update_price_feeds\",\"arguments\":\"eyJkYXRhIjoiNTA0ZTQxNTUwMTAwMDAwMDAzYjgwMTAwMDAwMDA0MGQwMDVkY2EyNzdhYjk1NjViMjI0ZDZkY2NjZjBlNGVlMDdhZDM1NDhhMDViMTAwNGNjY2ZmMWI4YTlmMWFiNWZmOWQ0YzYxMzdhNWZlYTYxYThlNTFhOTZhZGM1Yjg4MjU0MzE3YWEwZjM1MzJkN2ZmY2VkZGMwNWE1ZGUwZDlhNjRjMDAwMzM5MmU5MTk1NDVjM2Q1Y2JmYWVmOGUxNDkxMzlmY2JiMzQ3ZjI4YTU5ZDVhNWRhZTE3Y2VhNjFjMjFjNDU0N2I1NmY3MzQyNzVkMzAwNWQ1YTYyN2I3YTMwZmNlMjBmOTA5MjNjMjU3MWY4Yjk4MGUxYjVjNjQ4YjQ4Mjg0M2U0MDEwNGJhOTRmOWFiMzcxMjY3ODdlOTdlZmNkODlmMzU5OTdmYTc0NDI0N2FlNmQ5NTVlZGU3ZTVjNGFiNTE2ODA5N2YyZjNiMmM3ZTk1NmUzM2U3MzQzNDc3Mzk4YzhjNTZhN2U1YzM0MDFhZWFiNmY3ZDc4NmI1MWFmYzIzN2E5OGVhMDEwNjk4NTllMjMyNGFhNjM2YzI5NjU1YzJmOWQxMzgyZGExOTg4M2E2NWIyMzc1NWI4MzEzMmMzZDhhNDA4MjhiMDIxMTMzMTQxMmM0NzYxN2NlYWVkYTM3MTIxNjM2YmRkNjFjY2E2NzVkZWQwZTdmNjg1ZTc1OTJiYzY2OWIwNjI3MDAwODBmNzk1NTJhNjY4ZmM2YWEyMjVmNzkwODBjMmY1YzEzNmE2MDU1NjI3M2EwYzRjOWNlMTc2ODUzMDFiMGJlMTI1YWE2NTBjZDhlNzkxYTVhMGY0Yjg5ODdhZmZjNTFkMDdiMGYzNzcxMjAwMWUwNmI1MjRhYzkwMzI3Y2ZiMWFmMDAwYTczZTgxZjU1ODYwMGNiNGRkYTEwNTFjMWQ0MjBjNjQxNDgxNjVlZjM4MGVjNDU0ZDQwZjcwYTE4MTY5YWJmNzUyMWZkMzI4MWY5ZTM3YTRkMTM1YTU2Y2YwMDhjZDVkZGQ3ZmMzNTM2ZDU1M2QyODhlMmI0YjU5ZWRiMTA5NzVlMDAwYjEzYzI3YjA4Nzc5YTM4Nzk1ODdmMWVjMzNiNmU3YjVmNjgzY2I3NjRiOWM2YmVhNGEwMTExNmE4NjFjMjg1Yjc2MjhhMjUxMDk0NzI1YjFlOTY2Mjg3NThkYjg3YTg5MDY5OTQ5OTk4M2JiZTUxMmU2NGQxZjY2NTJkMDU1ZjQ0MDEwY2U3NWU3ZDFiNzRkZjFmMDRkYjZjZDhjNjU4Y2QwZmU5ODVjMjdkMjljYWM0OGU5MzI0ZDgxMGM5ZmZlYzJjMWEyYWQ2ZWYyYTRjNmRhZTMzMTIxYWY5NjUyZDJmYjk1YjZjN2FhZjA2MzQ3ZWE4OTU3ZDdhNzdhM2M5NGRjMTY3MDEwZDE3Yzk1NzBjZGZkOGI5Njc4ZjIyYTRlMGQzZDBmNWQ3ZTM1NzVmZjc1NzExODEyNTQzZDhlZWE3OWVjNzNkNWIzMmI0NTcwMDAwMDgyZjBiNTcwZmI4ZTRmMTFjOWE0ZTBiMmJkZGVlYmU0ZjQ4NDQxYzZjYWEyYzQ1ZDBmYTZmMDEwZTFkYjAyMWEzMzkyN2U1NmRlMGQ5OGJmMzZkMTUzNjEyMjM3N2NiNWU4NjQ3NzQ5NGJmMGYzZThhYWYyOWVhZTM3MGU2YmMzODc4ZWVmOTkxMjViMjk3NWU0OGY3MzhhYTg0MDNkOGEyZDhlMzFlNTMyMmY4NWNhZGFkZGMxMTEzMDAwZjFjZWIyYTBjZmU1ZTU0ZDRiYTIwMGRmY2Q2YzU3NmE3ZGViNzhkNGZiZTM5YTE4OWNlZDg1NDVjYWMzODYwMjg3MDE3NWQ1Y2M4YWZmNTRiMmNmNGRmZDUwYjc3YWFhMmRjZDk4YmVjZGEzODVlYWZhNGFhNjlkMzk1NDBiODJiMDAxMGVkNzBmNzY4OWQ1YTJkNzAxODJhZjVjMTAyYmZmZGI5ZGVmYzM2NDRiNzk0MGQ0ZmJmNDM4MzZiOWFkMzViZjM2ZGMwMTg0Y2Q4NTZjNDdmYWYzNWRlM2ZmYzg0YmExNzFkYWQxOWVmOTY2MTkxMDcyYWUxNmZlZmVhMzZiNmQ2MDAxMWJkY2RlOWExZWNmN2Q3ZjFlYjc3OTMzZDI5ZjA4MjFkNDE5NTFiZmFlYTA1YzEyZjc3ZmMyN2ZmNDA4YTA0NDc2ZGZiYmM0NWYwNWU3MmNiMGUwMzk4ZGIzOGMxZGM1OTZlY2IyMWJmNDhmN2I4NTU3MmE0N2Q5MjkyNzZlNGU1MDE2OTI5ODJkZjAwMDAwMDAwMDAxYWUxMDFmYWVkYWM1ODUxZTMyYjliMjNiNWY5NDExYThjMmJhYzRhYWUzZWQ0ZGQ3YjgxMWRkMWE3MmVhNGFhNzEwMDAwMDAwMDBhNGU0N2RlMDE0MTU1NTc1NjAwMDAwMDAwMDAwZjViZWViZjAwMDAyNzEwZTBiODlkNGFmNWYxMTA0MjJiZDUwMjM3ODdiYjFlMGE1MjMxODMxNDAyMDA1NTAwZWFhMDIwYzYxY2M0Nzk3MTI4MTM0NjFjZTE1Mzg5NGE5NmE2YzAwYjIxZWQwY2ZjMjc5OGQxZjlhOWU5Yzk0YTAwMDAwMDAwMDVmNTg5ZDYwMDAwMDAwMDAwMDEwNWQ1ZmZmZmZmZjgwMDAwMDAwMDY5Mjk4MmRmMDAwMDAwMDA2OTI5ODJkZjAwMDAwMDAwMDVmNThjOTIwMDAwMDAwMDAwMDExNjljMGRiOTVlZWM1NmYxMTkzNTZjY2YwZDdjNDg0ZmMyZTI0OTgzNTRjYjdmYzRjZTc2MTg5NzY0ZjJkMDNhODIwZTEwYmJhY2IwNzA0ZTJlNzAzNDYzNTE0NjVhZmY3Zjg2ZDQ1ZGUxY2FjMmQxYzhjMWEyMjk4NDljYTFkNjQ5ZmVjMGEwNWFiNDBmZTJjYzM0NWRkYjA2MGNmMjc0YjQ5ZmJlZmFjM2M1YjY5Njg2M2RlNzkwNDk2Nzc3NmRhMTRmYmFkMjJhODlhYjRmZGIyNzFmNzZjZWFjZjc2Y2M5MmQ0NDQ2NTgyZmE0NDU3NDlhZTliNTJhZWQxYTNiZWEzZjk4MWU4YjdkZmM0NjBjZDFlOWZlYmJjMWFjMDVjMjg0NzIzNGIwODZhY2U4MTRjZjQ0MTI0ZTM4OGExODllYTk0ODZjNTQ5N2ZkYzVjZTE4Y2Q0N2M4MDU5Njc4NTFiMTRhZDFjOGZkOWNmNTU0YjM5MjNmN2RhYjY5MmNjMjhkNzA4YTA2MDAwNzYzZmQyOWQxNDJjYWFjOGUxM2YwNTZmNWNmMDJhMDZjYmRjOTM1MzAzZjJmNGFiZmNhMzQ5NmY3OWNkY2MwYjZkZWY3Y2QxMjc0YWJmNjQ2NWMzZjM1N2UxNGNlNDc4MTlhNDVmOTcyZTk1ZTI0ZjYxYWY0ZjUxZjFmMjg0ZDQwMDA1NTAwYmU5YjU5ZDE3OGYwZDZhOTdhYjRjMzQzYmZmMmFhNjljYWExZWFhZTNlOTA0OGE2NTc4OGM1MjliMTI1YmIyNDAwMDAwMDBiMmRjNGQ3NTgwMDAwMDAwMDAzMjQ1ZDYxZmZmZmZmZjgwMDAwMDAwMDY5Mjk4MmRmMDAwMDAwMDA2OTI5ODJkZjAwMDAwMDBiMjZlZDM4YTgwMDAwMDAwMDAyYzE4Yzg0MGRhNDc0MTlkMTEyYWI4ZmI5Mjc1YjU2YmVhYzcxODkzMDlhMmY0ZjhmOGY2NjBmZmQ0YjMwMTIyZjRmN2ZkNTgyNjJjNjRkMTEyM2UwNjZmZDZkM2Q3NzAxYWQ1MjZmNDA5ZTMzNjE2NGI3Y2ZkYWM2NWQwZDZmYThkNDQ2M2I0MjFmYWYwMTQ1MjlkOWRmNWI1NDkxNWJlOTlkNDMzY2JiMDJjMGI2MGY3NGQzYzJhMTNiN2EyODQyOGZhYzE1N2ZkNTU0MTg2MzBiN2ZkNjk2ZWRiNjJmMTNhZGYzNjI4MDNjODUyMTYyZDg4NTQ1MmRhNzJkNzg0MGViMzQ1NjVhZjQ0MGM1OWUwOGJiYTAyYzk1ZThkZjdhYzQ2ZjY1MDg5ODg1OWU5NzI2MTAxNjIyNzA3ZjgxNTkyNzU0ZGVkMWQwYjc3OTBkOWFmODYyNjc2ODEyY2U1YTIwZjgxNGM0ZjBmM2M3ZGMyNDhlYmVjNTNlN2RiOWE3OTFlZjQ3YTAzYTY3NWQyOWE5MGNmYzYxNDJjYWFjOGUxM2YwNTZmNWNmMDJhMDZjYmRjOTM1MzAzZjJmNGFiZmNhMzQ5NmY3OWNkY2MwYjZkZWY3Y2QxMjc0YWJmNjQ2NWMzZjM1N2UxNGNlNDc4MTlhNDVmOTcyZTk1ZTI0ZjYxYWY0ZjUxZjFmMjg0ZDQwIn0=\",\"amount\":\"155000000000000\",\"gas\":\"155000000000000\"}}]},{\"receiver_id\":\"intents.near\",\"actions\":[{\"FunctionCall\":{\"function_name\":\"mt_transfer_call\",\"arguments\":\"eyJyZWNlaXZlcl9pZCI6Iml6ZWMtaXNvbHVzZGMudGVtcGxhci1hbHBoYS5uZWFyIiwiYW1vdW50IjoiMTcyMTc2NyIsIm1zZyI6IlwiUmVwYXlcIiIsInRva2VuX2lkIjoibmVwMTQxOnNvbC01Y2UzYmYzYTMxYWYxOGJlNDBiYTMwZjcyMTEwMWI0MzQxNjkwMTg2Lm9tZnQubmVhciJ9\",\"amount\":\"1\",\"gas\":\"50000000000000\"}}]},{\"receiver_id\":\"izec-isolusdc.templar-alpha.near\",\"actions\":[{\"FunctionCall\":{\"function_name\":\"withdraw_collateral\",\"arguments\":\"eyJhbW91bnQiOiI3MDUwMDAifQ==\",\"amount\":\"0\",\"gas\":\"50000000000000\"}}]}]}","signature":"ed25519:4CrFbqgiHo3BUv2QoHX7XDcRJqZeVvJJ8fB4SCgpzqSBPwsEyNCFT3uEKbwudDp2tzjQy9xPAeud6iq2qU1Crfet"}}"#)] diff --git a/universal-account/src/state/migration.rs b/universal-account/src/state/migration.rs index 8d2814d3a..40fda64bb 100644 --- a/universal-account/src/state/migration.rs +++ b/universal-account/src/state/migration.rs @@ -198,3 +198,64 @@ mod tests { assert_eq!(new.keys.len(), 1); } } + +#[cfg(kani)] +mod kani_proofs { + use near_sdk::{json_types::U128, store::IterableMap}; + use templar_common::versioned_state::StateTransformer; + + use crate::KeyId; + + use super::*; + + #[kani::proof] + fn v0_migration_preserves_scalar_safety_state() { + let next_key_index = kani::any::(); + let chain_id = kani::any::(); + let old = state::V0 { + next_key_index, + keys: IterableMap::::new(b"k"), + }; + + let new = V0 { + chain_id: U128(chain_id), + } + .transform(old) + .unwrap(); + + assert_eq!(new.next_key_index, next_key_index); + assert_eq!(new.chain_id, chain_id); + } + + #[kani::proof] + fn v1_migration_preserves_scalar_safety_state() { + let next_key_index = kani::any::(); + let chain_id = kani::any::(); + let old = state::V1 { + next_key_index, + keys: IterableMap::::new(b"k"), + chain_id, + }; + + let new = V1.transform(old).unwrap(); + + assert_eq!(new.next_key_index, next_key_index); + assert_eq!(new.chain_id, chain_id); + } + + #[kani::proof] + fn unbrick_v1_migration_preserves_scalar_safety_state() { + let next_key_index = kani::any::(); + let chain_id = kani::any::(); + let old = state::V1 { + next_key_index, + keys: IterableMap::::new(b"k"), + chain_id, + }; + + let new = UnbrickV1.transform(old).unwrap(); + + assert_eq!(new.next_key_index, next_key_index); + assert_eq!(new.chain_id, chain_id); + } +} From ed1aac9a3f76a6904ff69ad956bfa59f6834e9bc Mon Sep 17 00:00:00 2001 From: carrion256 Date: Thu, 18 Jun 2026 19:16:20 +0200 Subject: [PATCH 02/11] ENG-162 add Kani verification workflow --- .github/workflows/kani.yml | 83 ++++++++++++++++++++++++++++++++++++++ README.md | 1 + 2 files changed, 84 insertions(+) create mode 100644 .github/workflows/kani.yml diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml new file mode 100644 index 000000000..cc0dc0884 --- /dev/null +++ b/.github/workflows/kani.yml @@ -0,0 +1,83 @@ +name: Kani + +on: + schedule: + # Nightly verification on the default branch. + - cron: "0 2 * * *" + workflow_dispatch: + pull_request: + branches: [main, dev] + paths: + - ".github/workflows/kani.yml" + - "Cargo.toml" + - "Cargo.lock" + - "common/**" + - "contract/universal-account/**" + - "contract/vault/kernel/**" + - "fuzz/fuzz_targets/fuzz_fee_math.rs" + - "test-utils/src/controller/universal_account.rs" + - "universal-account/**" + +concurrency: + group: kani-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +env: + KANI_VERSION: "0.67.0" + CARGO_TERM_COLOR: always + CARGO_INCREMENTAL: 0 + +jobs: + universal-account: + name: Universal Account + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - name: Checkout repository + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 + with: + persist-credentials: false + + - name: Run Universal Account Kani proofs + uses: model-checking/kani-github-action@v1 + with: + kani-version: ${{ env.KANI_VERSION }} + command: cargo-kani + args: -p templar-universal-account + + vault-kernel: + name: Vault Kernel + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - name: Checkout repository + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 + with: + persist-credentials: false + + - name: Run Vault Kernel Kani proofs + uses: model-checking/kani-github-action@v1 + with: + kani-version: ${{ env.KANI_VERSION }} + command: cargo-kani + args: -p templar-vault-kernel + + vault-kernel-sync-external: + name: Vault Kernel / Sync External + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - name: Checkout repository + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 + with: + persist-credentials: false + + - name: Run Vault Kernel sync/rebalance Kani proofs + uses: model-checking/kani-github-action@v1 + with: + kani-version: ${{ env.KANI_VERSION }} + command: cargo-kani + args: -p templar-vault-kernel --features action-sync-external diff --git a/README.md b/README.md index e80e612c8..fe88808d3 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,7 @@ # Templar Protocol [![Test](https://github.com/Templar-Protocol/contracts/actions/workflows/test.yml/badge.svg)](https://github.com/Templar-Protocol/contracts/actions/workflows/test.yml) +[![Kani](https://github.com/Templar-Protocol/contracts/actions/workflows/kani.yml/badge.svg)](https://github.com/Templar-Protocol/contracts/actions/workflows/kani.yml) [![Coverage](https://codecov.io/gh/Templar-Protocol/contracts/branch/dev/graph/badge.svg)](https://codecov.io/gh/Templar-Protocol/contracts) [![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT) From d6ce78e1198252c952f783891e34074771193d9e Mon Sep 17 00:00:00 2001 From: carrion256 Date: Mon, 22 Jun 2026 12:42:29 +0200 Subject: [PATCH 03/11] ENG-162 fix Kani branch lint failures --- contract/universal-account/tests/universal_account.rs | 8 ++++---- contract/vault/kernel/src/math/number.rs | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/contract/universal-account/tests/universal_account.rs b/contract/universal-account/tests/universal_account.rs index b779cfc43..ff0543467 100644 --- a/contract/universal-account/tests/universal_account.rs +++ b/contract/universal-account/tests/universal_account.rs @@ -570,10 +570,10 @@ async fn key_indexes_are_unique_across_remove_and_readd() { ); assert_eq!(readded_entry.nonce.0, 0); - let keys = uac.list_keys(None, None).await; - assert_eq!(keys.len(), 2); - assert!(keys.contains(&key1)); - assert!(keys.contains(&key2)); + let listed_keys = uac.list_keys(None, None).await; + assert_eq!(listed_keys.len(), 2); + assert!(listed_keys.contains(&key1)); + assert!(listed_keys.contains(&key2)); } #[tokio::test] diff --git a/contract/vault/kernel/src/math/number.rs b/contract/vault/kernel/src/math/number.rs index 68a4578ad..8ad70e3a5 100644 --- a/contract/vault/kernel/src/math/number.rs +++ b/contract/vault/kernel/src/math/number.rs @@ -43,7 +43,7 @@ mod serde_impl { { struct NumberVisitor; - impl<'de> de::Visitor<'de> for NumberVisitor { + impl de::Visitor<'_> for NumberVisitor { type Value = Number; fn expecting(&self, formatter: &mut fmt::Formatter) -> fmt::Result { From e822b92abd49db992ae8f8f9e7e3eaeb45477e46 Mon Sep 17 00:00:00 2001 From: carrion256 Date: Tue, 23 Jun 2026 13:01:42 +0200 Subject: [PATCH 04/11] ENG-162 add semantic vault Kani proofs --- .github/workflows/kani.yml | 69 ++- contract/vault/kernel/Cargo.toml | 3 + contract/vault/kernel/src/lib.rs | 931 ++++++++++++++++++++++++++++++- 3 files changed, 997 insertions(+), 6 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index cc0dc0884..303cf975f 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -75,9 +75,74 @@ jobs: with: persist-credentials: false - - name: Run Vault Kernel sync/rebalance Kani proofs + - name: Run Vault Kernel external sync immutability Kani proof uses: model-checking/kani-github-action@v1 with: kani-version: ${{ env.KANI_VERSION }} command: cargo-kani - args: -p templar-vault-kernel --features action-sync-external + args: >- + -p templar-vault-kernel + --features action-sync-external + --harness sync_external_assets_only_mutates_external_and_total_assets_for_allowed_ops + + vault-kernel-allocation-lifecycle: + name: Vault Kernel / Allocation Lifecycle + runs-on: ubuntu-latest + timeout-minutes: 25 + steps: + - name: Checkout repository + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 + with: + persist-credentials: false + + - name: Run Vault Kernel allocation lifecycle Kani proofs + uses: model-checking/kani-github-action@v1 + with: + kani-version: ${{ env.KANI_VERSION }} + command: cargo-kani + args: >- + -p templar-vault-kernel + --features action-allocation-lifecycle,action-sync-external,action-recovery + --harness allocation_partial_sync_then_abort_restores_unallocated_assets + --harness allocation_full_sync_then_finish_conserves_assets + --harness allocation_wrong_op_id_is_rejected_without_progress + + vault-kernel-refresh-lifecycle: + name: Vault Kernel / Refresh Lifecycle + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - name: Checkout repository + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 + with: + persist-credentials: false + + - name: Run Vault Kernel refresh lifecycle Kani proofs + uses: model-checking/kani-github-action@v1 + with: + kani-version: ${{ env.KANI_VERSION }} + command: cargo-kani + args: >- + -p templar-vault-kernel + --features action-refresh-lifecycle,action-sync-external + --harness refresh_lifecycle_mutates_only_external_assets_and_returns_idle + + vault-kernel-refresh-fees: + name: Vault Kernel / Refresh Fees + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - name: Checkout repository + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 + with: + persist-credentials: false + + - name: Run Vault Kernel refresh fee Kani proofs + uses: model-checking/kani-github-action@v1 + with: + kani-version: ${{ env.KANI_VERSION }} + command: cargo-kani + args: >- + -p templar-vault-kernel + --features action-refresh-fees + --harness refresh_fees_zero_fee_rates_only_update_anchor diff --git a/contract/vault/kernel/Cargo.toml b/contract/vault/kernel/Cargo.toml index 539a6eac0..5b5c5e4f5 100644 --- a/contract/vault/kernel/Cargo.toml +++ b/contract/vault/kernel/Cargo.toml @@ -45,6 +45,9 @@ all-actions = [ "action-allocation-lifecycle", "action-refresh-lifecycle", ] +# Opt-in Kani harnesses that currently require queue/effect stubbing before +# they are suitable for regular CI. +kani-expensive-vault-proofs = [] [dependencies] derive_more.workspace = true diff --git a/contract/vault/kernel/src/lib.rs b/contract/vault/kernel/src/lib.rs index 0852cf774..4e726ae01 100644 --- a/contract/vault/kernel/src/lib.rs +++ b/contract/vault/kernel/src/lib.rs @@ -63,16 +63,17 @@ pub use transitions::{ #[cfg(kani)] mod kani_proofs { - #[cfg(feature = "action-sync-external")] - use alloc::vec::Vec; + use alloc::{vec, vec::Vec}; use super::*; + use crate::effects::{KernelEffect, KernelEvent}; const MAX_AMOUNT: u128 = 32; const OWNER: Address = Address([0x11; 32]); const RECEIVER: Address = Address([0x22; 32]); - #[cfg(feature = "action-sync-external")] const SELF: Address = Address([0x33; 32]); + const SECOND_OWNER: Address = Address([0x44; 32]); + const SECOND_RECEIVER: Address = Address([0x55; 32]); fn bounded_amount() -> u128 { let amount = kani::any::(); @@ -86,7 +87,6 @@ mod kani_proofs { amount } - #[cfg(feature = "action-sync-external")] fn zero_fee_config() -> VaultConfig { VaultConfig { fees: FeesSpec::zero(), @@ -99,6 +99,142 @@ mod kani_proofs { } } + #[cfg(all( + feature = "action-refresh-fees", + feature = "kani-expensive-vault-proofs" + ))] + fn bounded_fee_config() -> VaultConfig { + VaultConfig { + fees: FeesSpec::new( + FeeSlot::new(Wad(Number::from(1u128)), Address([0x66; 32])), + FeeSlot::new(Wad(Number::from(1u128)), Address([0x77; 32])), + None, + ), + min_withdrawal_assets: 0, + withdrawal_cooldown_ns: 0, + max_pending_withdrawals: 3, + paused: false, + virtual_shares: 0, + virtual_assets: 0, + } + } + + fn assert_accounting_invariant(state: &VaultState) { + assert!(state.check_invariant()); + assert_eq!( + state.total_assets, + state.idle_assets + state.external_assets + ); + } + + fn assert_asset_sum(state: &VaultState) { + assert_eq!( + state.total_assets, + state.idle_assets + state.external_assets + ); + } + + fn assert_address_eq(left: Address, right: Address) { + let mut index = 0usize; + while index < 32 { + assert_eq!(left.0[index], right.0[index]); + index += 1; + } + } + + fn address_eq(left: Address, right: Address) -> bool { + let mut index = 0usize; + while index < 32 { + if left.0[index] != right.0[index] { + return false; + } + index += 1; + } + true + } + + fn bounded_state() -> VaultState { + let idle = bounded_amount(); + let external = bounded_amount(); + let shares = bounded_amount(); + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO) + } + + fn allocation_plan(first: u128, second: u128) -> Vec { + vec![ + AllocationPlanEntry::new(0, first), + AllocationPlanEntry::new(1, second), + ] + } + + fn enqueue_withdrawal( + state: &mut VaultState, + owner: Address, + receiver: Address, + shares: u128, + expected_assets: u128, + requested_at_ns: TimestampNs, + ) -> u64 { + state + .withdraw_queue + .enqueue(owner, receiver, shares, expected_assets, requested_at_ns, 3) + .unwrap() + } + + fn refund_effect_sum(effects: &[KernelEffect], owner: Address) -> u128 { + let mut total = 0u128; + for effect in effects { + if let KernelEffect::TransferShares { from, to, shares } = effect { + if address_eq(*from, SELF) && address_eq(*to, owner) { + total += *shares; + } + } + } + total + } + + fn burn_effect_sum(effects: &[KernelEffect]) -> u128 { + let mut total = 0u128; + for effect in effects { + if let KernelEffect::BurnShares { owner, shares } = effect { + if address_eq(*owner, SELF) { + total += *shares; + } + } + } + total + } + + #[cfg(feature = "action-refresh-fees")] + fn minted_effect_sum(effects: &[KernelEffect]) -> u128 { + let mut total = 0u128; + for effect in effects { + if let KernelEffect::MintShares { shares, .. } = effect { + total += *shares; + } + } + total + } + + fn payout_event(effects: &[KernelEffect]) -> Option<(bool, u128, u128, u128)> { + for effect in effects { + if let KernelEffect::EmitEvent { + event: + KernelEvent::PayoutCompleted { + success, + burn_shares, + refund_shares, + amount, + .. + }, + } = effect + { + return Some((*success, *burn_shares, *refund_shares, *amount)); + } + } + None + } + #[kani::proof] fn bounded_initial_state_preserves_total_asset_invariant() { let idle = bounded_amount(); @@ -390,6 +526,793 @@ mod kani_proofs { ); assert_eq!(rebalanced.total_assets, idle + synced_external); } + + #[cfg(all( + feature = "action-allocation-lifecycle", + feature = "action-sync-external", + feature = "action-recovery" + ))] + #[kani::proof] + #[kani::unwind(8)] + fn allocation_partial_sync_then_abort_restores_unallocated_assets() { + let idle = nonzero_bounded_amount(); + let external = bounded_amount(); + let shares = bounded_amount(); + let first = nonzero_bounded_amount(); + let second = bounded_amount(); + kani::assume(first + second <= idle); + + let op_id = 11; + let state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + let started = apply_action( + state, + &zero_fee_config(), + None, + &SELF, + KernelAction::begin_allocating( + op_id, + allocation_plan(first, second), + TimestampNs::ZERO, + ), + ) + .unwrap() + .state; + + let stepped = allocation_step_callback(started.op_state.clone(), true, first, op_id) + .unwrap() + .new_state; + let mut after_step = started; + after_step.op_state = stepped; + + let synced = apply_action( + after_step, + &zero_fee_config(), + None, + &SELF, + KernelAction::sync_external_assets(external + first, op_id, TimestampNs::ZERO), + ) + .unwrap() + .state; + + let result = apply_action( + synced, + &zero_fee_config(), + None, + &SELF, + KernelAction::abort_allocating(op_id), + ) + .unwrap(); + + assert!(result.state.op_state.is_idle()); + assert_asset_sum(&result.state); + assert_eq!(result.state.idle_assets, idle - first); + assert_eq!(result.state.external_assets, external + first); + assert_eq!(result.state.total_assets, idle + external); + assert_eq!(result.state.total_shares, shares); + assert_eq!(result.state.withdraw_queue.status().length, 0); + } + + #[cfg(all( + feature = "action-allocation-lifecycle", + feature = "action-sync-external" + ))] + #[kani::proof] + #[kani::unwind(8)] + fn allocation_full_sync_then_finish_conserves_assets() { + let idle = nonzero_bounded_amount(); + let external = bounded_amount(); + let shares = bounded_amount(); + let first = nonzero_bounded_amount(); + let second = bounded_amount(); + kani::assume(first + second <= idle); + + let op_id = 12; + let state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + let started = apply_action( + state, + &zero_fee_config(), + None, + &SELF, + KernelAction::begin_allocating( + op_id, + allocation_plan(first, second), + TimestampNs::ZERO, + ), + ) + .unwrap() + .state; + + let stepped_once = allocation_step_callback(started.op_state.clone(), true, first, op_id) + .unwrap() + .new_state; + let stepped_twice = if second > 0 { + allocation_step_callback(stepped_once, true, second, op_id) + .unwrap() + .new_state + } else { + stepped_once + }; + let mut after_steps = started; + after_steps.op_state = stepped_twice; + + let synced = apply_action( + after_steps, + &zero_fee_config(), + None, + &SELF, + KernelAction::sync_external_assets(external + first + second, op_id, TimestampNs::ZERO), + ) + .unwrap() + .state; + + let result = apply_action( + synced, + &zero_fee_config(), + None, + &SELF, + KernelAction::finish_allocating(op_id, TimestampNs::ZERO), + ) + .unwrap(); + + assert!(result.state.op_state.is_idle()); + assert_asset_sum(&result.state); + assert_eq!(result.state.idle_assets, idle - first - second); + assert_eq!(result.state.external_assets, external + first + second); + assert_eq!(result.state.total_assets, idle + external); + assert_eq!(result.state.total_shares, shares); + } + + #[cfg(all( + feature = "action-allocation-lifecycle", + feature = "action-sync-external", + feature = "action-recovery" + ))] + #[kani::proof] + fn allocation_wrong_op_id_is_rejected_without_progress() { + let mut state = bounded_state(); + let op_id = 13; + let wrong_op_id = 14; + state.op_state = OpState::Allocating(AllocatingState { + op_id, + index: 0, + remaining: 1, + plan: allocation_plan(1, 0), + }); + let baseline = state.clone(); + + assert!(allocation_step_callback(state.op_state.clone(), true, 1, wrong_op_id).is_err()); + assert!(apply_action( + state.clone(), + &zero_fee_config(), + None, + &SELF, + KernelAction::sync_external_assets(1, wrong_op_id, TimestampNs::ZERO), + ) + .is_err()); + assert!(apply_action( + state.clone(), + &zero_fee_config(), + None, + &SELF, + KernelAction::finish_allocating(wrong_op_id, TimestampNs::ZERO), + ) + .is_err()); + assert!(apply_action( + state.clone(), + &zero_fee_config(), + None, + &SELF, + KernelAction::abort_allocating(wrong_op_id), + ) + .is_err()); + assert!(state == baseline); + } + + #[cfg(all(feature = "action-recovery", feature = "kani-expensive-vault-proofs"))] + #[kani::proof] + #[kani::unwind(40)] + fn abort_withdrawing_requires_fifo_head_identity_and_refunds_escrow() { + let idle = bounded_amount(); + let external = bounded_amount(); + let total_shares = nonzero_bounded_amount(); + let first_shares = nonzero_bounded_amount(); + let second_shares = nonzero_bounded_amount(); + let first_expected = nonzero_bounded_amount(); + let second_expected = nonzero_bounded_amount(); + let collected = bounded_amount(); + + let mut state = VaultState::with_initial( + idle + external, + total_shares, + idle, + external, + TimestampNs::ZERO, + ); + let first_id = enqueue_withdrawal( + &mut state, + OWNER, + RECEIVER, + first_shares, + first_expected, + TimestampNs::ZERO, + ); + let second_id = enqueue_withdrawal( + &mut state, + SECOND_OWNER, + SECOND_RECEIVER, + second_shares, + second_expected, + TimestampNs::ZERO, + ); + + let op_id = 21; + let mismatched = WithdrawingState { + op_id, + request_id: second_id, + index: 0, + remaining: second_expected, + collected, + receiver: SECOND_RECEIVER, + owner: SECOND_OWNER, + escrow_shares: second_shares, + }; + let mut mismatch_state = state.clone(); + mismatch_state.op_state = OpState::Withdrawing(mismatched); + assert!(apply_action( + mismatch_state, + &zero_fee_config(), + None, + &SELF, + KernelAction::abort_withdrawing(op_id), + ) + .is_err()); + + let mut valid_state = state.clone(); + valid_state.op_state = OpState::Withdrawing(WithdrawingState { + op_id, + request_id: first_id, + index: 0, + remaining: first_expected, + collected, + receiver: RECEIVER, + owner: OWNER, + escrow_shares: first_shares, + }); + let result = apply_action( + valid_state, + &zero_fee_config(), + None, + &SELF, + KernelAction::abort_withdrawing(op_id), + ) + .unwrap(); + + assert!(result.state.op_state.is_idle()); + assert_asset_sum(&result.state); + assert_eq!(result.state.idle_assets, idle + collected); + assert_eq!(result.state.external_assets, external); + assert_eq!(result.state.total_shares, total_shares); + assert_eq!(refund_effect_sum(&result.effects, OWNER), first_shares); + assert_eq!(result.state.withdraw_queue.status().length, 1); + assert_eq!( + result.state.withdraw_queue.head().map(|(id, _)| id), + Some(second_id) + ); + } + + #[kani::proof] + fn withdrawal_collection_preserves_collected_plus_remaining() { + let amount = nonzero_bounded_amount(); + let first_collect = bounded_amount(); + let burn_shares = bounded_amount(); + let escrow_shares = nonzero_bounded_amount(); + kani::assume(first_collect <= amount); + kani::assume(burn_shares <= escrow_shares); + + let op_id = 31; + let request = WithdrawalRequest { + op_id, + request_id: 0, + amount, + receiver: RECEIVER, + owner: OWNER, + escrow_shares, + }; + + let started = start_withdrawal(OpState::Idle, request).unwrap().new_state; + let stepped = withdrawal_step_callback(started, op_id, first_collect) + .unwrap() + .new_state; + let withdrawing = stepped.as_withdrawing().unwrap(); + assert_eq!(withdrawing.collected + withdrawing.remaining, amount); + + if withdrawing.remaining > 0 { + assert!(withdrawal_collected(stepped.clone(), op_id, burn_shares).is_err()); + } + + let completed = withdrawal_step_callback(stepped, op_id, amount - first_collect) + .unwrap() + .new_state; + let payout = withdrawal_collected(completed, op_id, burn_shares) + .unwrap() + .new_state; + let payout = payout.as_payout().unwrap(); + assert_eq!(payout.amount, amount); + assert_eq!(payout.burn_shares, burn_shares); + assert!(payout.burn_shares <= payout.escrow_shares); + } + + #[cfg(feature = "kani-expensive-vault-proofs")] + fn payout_state( + idle: u128, + external: u128, + total_shares: u128, + escrow_shares: u128, + burn_shares: u128, + amount: u128, + op_id: u64, + ) -> VaultState { + let mut state = VaultState::with_initial( + idle + external, + total_shares, + idle, + external, + TimestampNs::ZERO, + ); + let request_id = enqueue_withdrawal( + &mut state, + OWNER, + RECEIVER, + escrow_shares, + amount, + TimestampNs::ZERO, + ); + state.op_state = OpState::Payout(PayoutState { + op_id, + request_id, + receiver: RECEIVER, + amount, + owner: OWNER, + escrow_shares, + burn_shares, + }); + state + } + + #[cfg(feature = "kani-expensive-vault-proofs")] + #[kani::proof] + #[kani::unwind(40)] + fn payout_success_settlement_conserves_assets_and_escrow() { + let idle = nonzero_bounded_amount(); + let external = bounded_amount(); + let total_shares = nonzero_bounded_amount(); + let escrow_shares = nonzero_bounded_amount(); + let burn_shares = bounded_amount(); + let amount = bounded_amount(); + kani::assume(burn_shares <= escrow_shares); + kani::assume(burn_shares <= total_shares); + kani::assume(amount <= idle); + + let op_id = 41; + let success = apply_action( + payout_state( + idle, + external, + total_shares, + escrow_shares, + burn_shares, + amount, + op_id, + ), + &zero_fee_config(), + None, + &SELF, + KernelAction::settle_payout(op_id, PayoutOutcome::Success), + ) + .unwrap(); + assert!(success.state.op_state.is_idle()); + assert_asset_sum(&success.state); + assert_eq!(success.state.idle_assets, idle - amount); + assert_eq!(success.state.external_assets, external); + assert_eq!(success.state.total_assets, idle + external - amount); + assert_eq!(success.state.total_shares, total_shares - burn_shares); + assert_eq!(success.state.withdraw_queue.status().length, 0); + assert_eq!(burn_effect_sum(&success.effects), burn_shares); + assert_eq!( + refund_effect_sum(&success.effects, OWNER), + escrow_shares - burn_shares + ); + assert_eq!( + payout_event(&success.effects), + Some((true, burn_shares, escrow_shares - burn_shares, amount)) + ); + } + + #[cfg(feature = "kani-expensive-vault-proofs")] + #[kani::proof] + #[kani::unwind(40)] + fn payout_failure_settlement_refunds_without_mutating_assets_or_shares() { + let idle = nonzero_bounded_amount(); + let external = bounded_amount(); + let total_shares = nonzero_bounded_amount(); + let escrow_shares = nonzero_bounded_amount(); + let burn_shares = bounded_amount(); + let amount = bounded_amount(); + kani::assume(burn_shares <= escrow_shares); + kani::assume(burn_shares <= total_shares); + kani::assume(amount <= idle); + + let op_id = 42; + let failure = apply_action( + payout_state( + idle, + external, + total_shares, + escrow_shares, + burn_shares, + amount, + op_id, + ), + &zero_fee_config(), + None, + &SELF, + KernelAction::settle_payout(op_id, PayoutOutcome::Failure), + ) + .unwrap(); + assert!(failure.state.op_state.is_idle()); + assert_asset_sum(&failure.state); + assert_eq!(failure.state.idle_assets, idle); + assert_eq!(failure.state.external_assets, external); + assert_eq!(failure.state.total_assets, idle + external); + assert_eq!(failure.state.total_shares, total_shares); + assert_eq!(failure.state.withdraw_queue.status().length, 0); + assert_eq!(burn_effect_sum(&failure.effects), 0); + assert_eq!(refund_effect_sum(&failure.effects, OWNER), escrow_shares); + assert_eq!( + payout_event(&failure.effects), + Some((false, 0, escrow_shares, 0)) + ); + } + + #[cfg(all(feature = "action-recovery", feature = "kani-expensive-vault-proofs"))] + #[kani::proof] + #[kani::unwind(40)] + fn emergency_reset_recovers_non_idle_states_without_share_or_queue_leakage() { + let idle = bounded_amount(); + let external = bounded_amount(); + let shares = nonzero_bounded_amount(); + let amount = bounded_amount(); + let escrow = nonzero_bounded_amount(); + let kind = kani::any::(); + kani::assume(kind < 4); + + let mut state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + let op_id = 51; + let expected_idle_restore; + let expected_refund; + let expected_queue_len; + + if kind == 0 { + state.op_state = OpState::Allocating(AllocatingState { + op_id, + index: 0, + remaining: amount, + plan: allocation_plan(amount, 0), + }); + expected_idle_restore = amount; + expected_refund = 0; + expected_queue_len = 0; + } else if kind == 1 { + let request_id = enqueue_withdrawal( + &mut state, + OWNER, + RECEIVER, + escrow, + amount, + TimestampNs::ZERO, + ); + state.op_state = OpState::Withdrawing(WithdrawingState { + op_id, + request_id, + index: 0, + remaining: amount, + collected: amount, + receiver: RECEIVER, + owner: OWNER, + escrow_shares: escrow, + }); + expected_idle_restore = amount; + expected_refund = escrow; + expected_queue_len = 0; + } else if kind == 2 { + let request_id = enqueue_withdrawal( + &mut state, + OWNER, + RECEIVER, + escrow, + amount, + TimestampNs::ZERO, + ); + state.op_state = OpState::Payout(PayoutState { + op_id, + request_id, + receiver: RECEIVER, + amount, + owner: OWNER, + escrow_shares: escrow, + burn_shares: 0, + }); + expected_idle_restore = amount; + expected_refund = escrow; + expected_queue_len = 0; + } else { + state.op_state = OpState::Refreshing(RefreshingState { + op_id, + index: 0, + plan: vec![0], + }); + expected_idle_restore = 0; + expected_refund = 0; + expected_queue_len = 0; + } + + let result = apply_action( + state, + &zero_fee_config(), + None, + &SELF, + KernelAction::emergency_reset(), + ) + .unwrap(); + + assert!(result.state.op_state.is_idle()); + assert_asset_sum(&result.state); + assert_eq!(result.state.idle_assets, idle + expected_idle_restore); + assert_eq!(result.state.external_assets, external); + assert_eq!(result.state.total_shares, shares); + assert_eq!( + result.state.withdraw_queue.status().length, + expected_queue_len + ); + assert_eq!(refund_effect_sum(&result.effects, OWNER), expected_refund); + assert_eq!( + result.state.fee_anchor.total_assets, + result.state.total_assets + ); + } + + #[cfg(feature = "action-sync-external")] + #[kani::proof] + #[kani::unwind(40)] + fn sync_external_assets_only_mutates_external_and_total_assets_for_allowed_ops() { + let idle = bounded_amount(); + let external = bounded_amount(); + let synced_external = bounded_amount(); + let shares = bounded_amount(); + let op_kind = kani::any::(); + kani::assume(op_kind < 3); + + let mut state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + let op_id = 61; + if op_kind == 0 { + state.op_state = OpState::Allocating(AllocatingState { + op_id, + index: 1, + remaining: 2, + plan: allocation_plan(1, 1), + }); + } else if op_kind == 1 { + let request_id = + enqueue_withdrawal(&mut state, OWNER, RECEIVER, 3, 4, TimestampNs::ZERO); + state.op_state = OpState::Withdrawing(WithdrawingState { + op_id, + request_id, + index: 1, + remaining: 2, + collected: 2, + receiver: RECEIVER, + owner: OWNER, + escrow_shares: 3, + }); + } else { + state.op_state = OpState::Refreshing(RefreshingState { + op_id, + index: 1, + plan: vec![7, 8], + }); + } + + let before_idle = state.idle_assets; + let before_shares = state.total_shares; + let before_queue = state.withdraw_queue.status(); + let before_next_op_id = state.next_op_id; + let before_fee_anchor_total_assets = state.fee_anchor.total_assets; + let before_fee_anchor_timestamp = state.fee_anchor.timestamp_ns; + let result = apply_action( + state, + &zero_fee_config(), + None, + &SELF, + KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO), + ) + .unwrap(); + + assert_eq!(result.state.idle_assets, before_idle); + assert_eq!(result.state.external_assets, synced_external); + assert_eq!(result.state.total_assets, before_idle + synced_external); + assert_eq!(result.state.total_shares, before_shares); + assert_eq!( + result.state.withdraw_queue.status().length, + before_queue.length + ); + assert_eq!( + result.state.withdraw_queue.status().total_escrow_shares, + before_queue.total_escrow_shares + ); + assert_eq!( + result.state.withdraw_queue.status().total_expected_assets, + before_queue.total_expected_assets + ); + assert_eq!(result.state.next_op_id, before_next_op_id); + assert_eq!( + result.state.fee_anchor.total_assets, + before_fee_anchor_total_assets + ); + assert!(result.state.fee_anchor.timestamp_ns == before_fee_anchor_timestamp); + match &result.state.op_state { + OpState::Allocating(alloc) => { + assert_eq!(op_kind, 0); + assert_eq!(alloc.op_id, op_id); + assert_eq!(alloc.index, 1); + assert_eq!(alloc.remaining, 2); + } + OpState::Withdrawing(withdraw) => { + assert_eq!(op_kind, 1); + assert_eq!(withdraw.op_id, op_id); + assert_eq!(withdraw.index, 1); + assert_eq!(withdraw.remaining, 2); + assert_eq!(withdraw.collected, 2); + assert_address_eq(withdraw.owner, OWNER); + assert_address_eq(withdraw.receiver, RECEIVER); + assert_eq!(withdraw.escrow_shares, 3); + } + OpState::Refreshing(refresh) => { + assert_eq!(op_kind, 2); + assert_eq!(refresh.op_id, op_id); + assert_eq!(refresh.index, 1); + } + _ => panic!("sync must preserve active operation kind"), + } + assert_asset_sum(&result.state); + + let idle_state = VaultState::with_initial( + before_idle + synced_external, + before_shares, + before_idle, + synced_external, + TimestampNs::ZERO, + ); + assert!(apply_action( + idle_state, + &zero_fee_config(), + None, + &SELF, + KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO), + ) + .is_err()); + } + + #[cfg(all(feature = "action-refresh-lifecycle", feature = "action-sync-external"))] + #[kani::proof] + #[kani::unwind(8)] + fn refresh_lifecycle_mutates_only_external_assets_and_returns_idle() { + let idle = bounded_amount(); + let external = bounded_amount(); + let synced_external = bounded_amount(); + let shares = bounded_amount(); + let op_id = 71; + + let state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + let started = apply_action( + state, + &zero_fee_config(), + None, + &SELF, + KernelAction::begin_refreshing(op_id, vec![1, 2], TimestampNs::ZERO), + ) + .unwrap() + .state; + assert!(started.op_state.is_refreshing()); + assert_eq!(started.idle_assets, idle); + assert_eq!(started.external_assets, external); + assert_eq!(started.total_assets, idle + external); + assert_eq!(started.total_shares, shares); + + let synced = apply_action( + started, + &zero_fee_config(), + None, + &SELF, + KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO), + ) + .unwrap() + .state; + + let result = apply_action( + synced, + &zero_fee_config(), + None, + &SELF, + KernelAction::finish_refreshing(op_id, TimestampNs::ZERO), + ) + .unwrap(); + + assert!(result.state.op_state.is_idle()); + assert_eq!(result.state.idle_assets, idle); + assert_eq!(result.state.external_assets, synced_external); + assert_eq!(result.state.total_assets, idle + synced_external); + assert_eq!(result.state.total_shares, shares); + assert_asset_sum(&result.state); + } + + #[cfg(feature = "action-refresh-fees")] + #[kani::proof] + #[kani::unwind(8)] + fn refresh_fees_zero_fee_rates_only_update_anchor() { + let idle = bounded_amount(); + let external = bounded_amount(); + let shares = nonzero_bounded_amount(); + let anchor_assets = bounded_amount(); + let now = TimestampNs::from_nanos(1); + + let mut state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + state.fee_anchor = FeeAccrualAnchor::new(anchor_assets, TimestampNs::ZERO); + let before = state.clone(); + let before_queue = before.withdraw_queue.status(); + + let result = apply_action( + state, + &zero_fee_config(), + None, + &SELF, + KernelAction::refresh_fees(now), + ) + .unwrap(); + + let minted = minted_effect_sum(&result.effects); + assert_eq!(result.state.idle_assets, before.idle_assets); + assert_eq!(result.state.external_assets, before.external_assets); + assert_eq!(result.state.total_assets, before.total_assets); + assert_eq!(minted, 0); + assert_eq!(result.state.total_shares, before.total_shares); + assert_eq!( + result.state.fee_anchor.total_assets, + result.state.total_assets + ); + assert!(result.state.fee_anchor.timestamp_ns == now); + assert!(result.state.fee_anchor.timestamp_ns > before.fee_anchor.timestamp_ns); + assert!(result.state.op_state.is_idle()); + assert_eq!( + result.state.withdraw_queue.status().length, + before_queue.length + ); + assert_eq!( + result.state.withdraw_queue.status().total_escrow_shares, + before_queue.total_escrow_shares + ); + assert_eq!( + result.state.withdraw_queue.status().total_expected_assets, + before_queue.total_expected_assets + ); + assert_eq!(result.state.next_op_id, before.next_op_id); + assert_asset_sum(&result.state); + } } pub use types::{ActualIdx, Address, AssetId, DurationNs, ExpectedIdx, KernelVersion, TimestampNs}; pub use utils::TimeGate; From 172f5f0f2146291eeb3093be0d492fd18f08f442 Mon Sep 17 00:00:00 2001 From: carrion256 Date: Tue, 23 Jun 2026 16:48:21 +0200 Subject: [PATCH 05/11] ENG-162 strengthen curated vault Kani invariants --- .github/workflows/kani.yml | 29 +- contract/vault/kernel/Cargo.toml | 4 - contract/vault/kernel/src/actions/mod.rs | 169 ++-- contract/vault/kernel/src/lib.rs | 1120 ++++++++++++++-------- 4 files changed, 864 insertions(+), 458 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 303cf975f..b9d253e6c 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -83,7 +83,10 @@ jobs: args: >- -p templar-vault-kernel --features action-sync-external - --harness sync_external_assets_only_mutates_external_and_total_assets_for_allowed_ops + --harness sync_external_assets_allocating_only_mutates_external_and_total_assets + --harness sync_external_assets_withdrawing_preserves_share_supply_queue_and_actor_fields + --harness sync_external_assets_refreshing_only_mutates_external_and_total_assets + --harness sync_external_assets_rejects_wrong_op_id_and_disallowed_states vault-kernel-allocation-lifecycle: name: Vault Kernel / Allocation Lifecycle @@ -127,6 +130,29 @@ jobs: --features action-refresh-lifecycle,action-sync-external --harness refresh_lifecycle_mutates_only_external_assets_and_returns_idle + vault-kernel-recovery: + name: Vault Kernel / Recovery + runs-on: ubuntu-latest + timeout-minutes: 25 + steps: + - name: Checkout repository + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 + with: + persist-credentials: false + + - name: Run Vault Kernel emergency recovery Kani proofs + uses: model-checking/kani-github-action@v1 + with: + kani-version: ${{ env.KANI_VERSION }} + command: cargo-kani + args: >- + -p templar-vault-kernel + --features action-recovery + --harness emergency_reset_allocating_restores_remaining_assets_to_idle + --harness emergency_reset_withdrawing_restores_collected_assets_and_refunds_escrow + --harness emergency_reset_payout_restores_payout_assets_and_refunds_escrow + --harness emergency_reset_refreshing_returns_idle_without_accounting_mutation + vault-kernel-refresh-fees: name: Vault Kernel / Refresh Fees runs-on: ubuntu-latest @@ -146,3 +172,4 @@ jobs: -p templar-vault-kernel --features action-refresh-fees --harness refresh_fees_zero_fee_rates_only_update_anchor + --harness refresh_fees_active_rates_only_mint_fee_shares_and_update_anchor diff --git a/contract/vault/kernel/Cargo.toml b/contract/vault/kernel/Cargo.toml index 5b5c5e4f5..fc1761789 100644 --- a/contract/vault/kernel/Cargo.toml +++ b/contract/vault/kernel/Cargo.toml @@ -45,10 +45,6 @@ all-actions = [ "action-allocation-lifecycle", "action-refresh-lifecycle", ] -# Opt-in Kani harnesses that currently require queue/effect stubbing before -# they are suitable for regular CI. -kani-expensive-vault-proofs = [] - [dependencies] derive_more.workspace = true primitive-types = { version = "0.14.0", default-features = false } diff --git a/contract/vault/kernel/src/actions/mod.rs b/contract/vault/kernel/src/actions/mod.rs index 2684286da..cf47a53f6 100644 --- a/contract/vault/kernel/src/actions/mod.rs +++ b/contract/vault/kernel/src/actions/mod.rs @@ -89,13 +89,13 @@ enum WithdrawalQueueOutcome { #[cfg_attr(not(target_arch = "wasm32"), derive(Debug))] #[derive(Clone, Copy, PartialEq, Eq)] -struct PendingWithdrawalHead { - id: u64, - owner: Address, - receiver: Address, - escrow_shares: u128, - expected_assets: u128, - requested_at_ns: TimestampNs, +pub(crate) struct PendingWithdrawalHead { + pub(crate) id: u64, + pub(crate) owner: Address, + pub(crate) receiver: Address, + pub(crate) escrow_shares: u128, + pub(crate) expected_assets: u128, + pub(crate) requested_at_ns: TimestampNs, } #[cfg_attr(not(target_arch = "wasm32"), derive(Debug))] @@ -109,20 +109,31 @@ enum WithdrawalHeadOutcome { #[cfg_attr(not(target_arch = "wasm32"), derive(Debug))] #[derive(Clone, Copy, PartialEq, Eq)] -struct PayoutSettlement { - burn_shares: u128, - refund_shares: u128, - completed_amount: u128, - success: bool, +pub(crate) struct PayoutSettlement { + pub(crate) burn_shares: u128, + pub(crate) refund_shares: u128, + pub(crate) completed_amount: u128, + pub(crate) success: bool, +} + +#[cfg_attr(not(target_arch = "wasm32"), derive(Debug))] +#[derive(Clone, PartialEq, Eq)] +#[cfg(any(feature = "action-recovery", test))] +pub(crate) struct EmergencyResetOutcome { + pub(crate) state: VaultState, + pub(crate) op_id: u64, + pub(crate) from_code: u32, + pub(crate) refund_owner: Option
, + pub(crate) refund_shares: u128, } #[cfg_attr(not(target_arch = "wasm32"), derive(Debug))] #[derive(Clone, Copy, PartialEq, Eq)] -struct WithdrawalRequestPlan { - owner: Address, - receiver: Address, - shares: u128, - expected_assets: u128, +pub(crate) struct WithdrawalRequestPlan { + pub(crate) owner: Address, + pub(crate) receiver: Address, + pub(crate) shares: u128, + pub(crate) expected_assets: u128, } #[cfg_attr(not(target_arch = "wasm32"), derive(Debug))] @@ -614,7 +625,7 @@ fn check_op_id(expected: u64, actual: u64) -> Result<(), KernelError> { /// /// Used by both `AbortWithdrawing` and `SettlePayout` to ensure consistency /// between the op-state and the queue. -fn validate_queue_head( +pub(crate) fn validate_queue_head( queue: &WithdrawQueue, request_id: u64, owner: &Address, @@ -914,7 +925,7 @@ fn dequeue_skipped_withdrawal( } #[inline] -fn pending_withdrawal_head(state: &VaultState) -> Option { +pub(crate) fn pending_withdrawal_head(state: &VaultState) -> Option { state .withdraw_queue .head() @@ -962,7 +973,7 @@ fn has_actionable_withdrawal_liquidity(expected_assets: u128, available_assets: } #[inline] -fn withdrawal_request_from_head( +pub(crate) fn withdrawal_request_from_head( state: &mut VaultState, head: PendingWithdrawalHead, ) -> WithdrawalRequest { @@ -1013,6 +1024,46 @@ fn plan_withdrawal_request( }) } +#[inline] +pub(crate) fn apply_withdrawal_request_plan( + mut state: VaultState, + config: &VaultConfig, + self_id: &Address, + request_plan: WithdrawalRequestPlan, + now_ns: TimestampNs, +) -> Result { + let id = state + .withdraw_queue + .enqueue( + request_plan.owner, + request_plan.receiver, + request_plan.shares, + request_plan.expected_assets, + now_ns, + config.max_pending_withdrawals, + ) + .map_err(map_queue_error)?; + + let effects = vec![ + KernelEffect::TransferShares { + from: request_plan.owner, + to: *self_id, + shares: request_plan.shares, + }, + KernelEffect::EmitEvent { + event: crate::effects::KernelEvent::WithdrawalRequested { + id, + owner: request_plan.owner, + receiver: request_plan.receiver, + shares: request_plan.shares, + expected_assets: request_plan.expected_assets, + }, + }, + ]; + + Ok(KernelResult::new(state, effects)) +} + #[inline] #[cfg(any(feature = "action-sync-external", test))] fn ensure_sync_external_state_allowed(op_state: &OpState) -> Result<(), KernelError> { @@ -1221,7 +1272,7 @@ fn handle_atomic_redeem( /// Enqueue a withdrawal request: validate, compute expected assets, escrow shares. #[allow(clippy::too_many_arguments)] fn handle_request_withdraw( - mut state: VaultState, + state: VaultState, config: &VaultConfig, restrictions: Option<&Restrictions>, self_id: &Address, @@ -1247,36 +1298,7 @@ fn handle_request_withdraw( let request_plan = plan_withdrawal_request(&state, config, owner, receiver, shares, min_assets_out)?; - let id = state - .withdraw_queue - .enqueue( - request_plan.owner, - request_plan.receiver, - request_plan.shares, - request_plan.expected_assets, - now_ns, - config.max_pending_withdrawals, - ) - .map_err(map_queue_error)?; - - let effects = vec![ - KernelEffect::TransferShares { - from: request_plan.owner, - to: *self_id, - shares: request_plan.shares, - }, - KernelEffect::EmitEvent { - event: crate::effects::KernelEvent::WithdrawalRequested { - id, - owner: request_plan.owner, - receiver: request_plan.receiver, - shares: request_plan.shares, - expected_assets: request_plan.expected_assets, - }, - }, - ]; - - Ok(KernelResult::new(state, effects)) + apply_withdrawal_request_plan(state, config, self_id, request_plan, now_ns) } /// Execute the next queued withdrawal after cooldown. @@ -1547,7 +1569,7 @@ fn handle_abort_withdrawing( } #[inline] -fn plan_payout_settlement( +pub(crate) fn plan_payout_settlement( payout: &PayoutState, outcome: PayoutOutcome, ) -> Result { @@ -1576,7 +1598,7 @@ fn plan_payout_settlement( } } -fn apply_payout_settlement( +pub(crate) fn apply_payout_settlement( state: &mut VaultState, payout: &PayoutState, settlement: PayoutSettlement, @@ -1756,10 +1778,9 @@ fn handle_refresh_fees( } #[cfg(any(feature = "action-recovery", test))] -fn handle_emergency_reset( +pub(crate) fn plan_emergency_reset( mut state: VaultState, - self_id: &Address, -) -> Result { +) -> Result { let prev_state = mem::take(&mut state.op_state); let from_code = prev_state.kind_code(); let op_id = match prev_state.op_id() { @@ -1771,8 +1792,8 @@ fn handle_emergency_reset( } }; - let mut effects = Vec::new(); - let escrow_address = *self_id; + let mut refund_owner = None; + let mut refund_shares = 0; match prev_state { OpState::Idle => { @@ -1788,13 +1809,15 @@ fn handle_emergency_reset( state.restore_to_idle(alloc.remaining); } OpState::Withdrawing(w) => { - push_refund_shares(&mut effects, escrow_address, w.owner, w.escrow_shares); + refund_owner = Some(w.owner); + refund_shares = w.escrow_shares; // Restore any collected assets back to idle. state.restore_to_idle(w.collected); state.withdraw_queue.dequeue(); } OpState::Payout(p) => { - push_refund_shares(&mut effects, escrow_address, p.owner, p.escrow_shares); + refund_owner = Some(p.owner); + refund_shares = p.escrow_shares; // Restore payout amount back to idle. state.restore_to_idle(p.amount); state.withdraw_queue.dequeue(); @@ -1803,14 +1826,34 @@ fn handle_emergency_reset( state.op_state = OpState::Idle; state.fee_anchor = FeeAccrualAnchor::new(state.total_assets, state.fee_anchor.timestamp_ns); + + Ok(EmergencyResetOutcome { + state, + op_id, + from_code, + refund_owner, + refund_shares, + }) +} + +#[cfg(any(feature = "action-recovery", test))] +pub(crate) fn handle_emergency_reset( + state: VaultState, + self_id: &Address, +) -> Result { + let outcome = plan_emergency_reset(state)?; + let mut effects = Vec::new(); + if let Some(owner) = outcome.refund_owner { + push_refund_shares(&mut effects, *self_id, owner, outcome.refund_shares); + } effects.push(KernelEffect::EmitEvent { event: KernelEvent::EmergencyResetCompleted { - op_id, - from_state: from_code, + op_id: outcome.op_id, + from_state: outcome.from_code, }, }); - Ok(KernelResult::new(state, effects)) + Ok(KernelResult::new(outcome.state, effects)) } /// Apply a kernel action to state, returning updated state and effects. diff --git a/contract/vault/kernel/src/lib.rs b/contract/vault/kernel/src/lib.rs index 4e726ae01..aeceb8153 100644 --- a/contract/vault/kernel/src/lib.rs +++ b/contract/vault/kernel/src/lib.rs @@ -66,7 +66,14 @@ mod kani_proofs { use alloc::{vec, vec::Vec}; use super::*; - use crate::effects::{KernelEffect, KernelEvent}; + #[cfg(feature = "action-recovery")] + use crate::actions::plan_emergency_reset; + use crate::actions::{ + apply_payout_settlement, apply_withdrawal_request_plan, pending_withdrawal_head, + plan_payout_settlement, validate_queue_head, withdrawal_request_from_head, + WithdrawalRequestPlan, + }; + use crate::effects::KernelEffect; const MAX_AMOUNT: u128 = 32; const OWNER: Address = Address([0x11; 32]); @@ -99,15 +106,12 @@ mod kani_proofs { } } - #[cfg(all( - feature = "action-refresh-fees", - feature = "kani-expensive-vault-proofs" - ))] - fn bounded_fee_config() -> VaultConfig { + #[cfg(feature = "action-refresh-fees")] + fn active_fee_config() -> VaultConfig { VaultConfig { fees: FeesSpec::new( - FeeSlot::new(Wad(Number::from(1u128)), Address([0x66; 32])), - FeeSlot::new(Wad(Number::from(1u128)), Address([0x77; 32])), + FeeSlot::new(Wad::one() / 10, Address([0x66; 32])), + FeeSlot::new(Wad::one() / 20, Address([0x77; 32])), None, ), min_withdrawal_assets: 0, @@ -142,17 +146,6 @@ mod kani_proofs { } } - fn address_eq(left: Address, right: Address) -> bool { - let mut index = 0usize; - while index < 32 { - if left.0[index] != right.0[index] { - return false; - } - index += 1; - } - true - } - fn bounded_state() -> VaultState { let idle = bounded_amount(); let external = bounded_amount(); @@ -181,58 +174,43 @@ mod kani_proofs { .unwrap() } - fn refund_effect_sum(effects: &[KernelEffect], owner: Address) -> u128 { - let mut total = 0u128; - for effect in effects { - if let KernelEffect::TransferShares { from, to, shares } = effect { - if address_eq(*from, SELF) && address_eq(*to, owner) { - total += *shares; - } + fn assert_transfer_shares_effect( + effect: &KernelEffect, + expected_from: Address, + expected_to: Address, + expected_shares: u128, + ) { + match effect { + KernelEffect::TransferShares { from, to, shares } => { + assert_address_eq(*from, expected_from); + assert_address_eq(*to, expected_to); + assert_eq!(*shares, expected_shares); } + _ => panic!("expected transfer shares effect"), } - total } - fn burn_effect_sum(effects: &[KernelEffect]) -> u128 { - let mut total = 0u128; - for effect in effects { - if let KernelEffect::BurnShares { owner, shares } = effect { - if address_eq(*owner, SELF) { - total += *shares; - } - } + fn assert_emit_event_effect(effect: &KernelEffect) { + match effect { + KernelEffect::EmitEvent { .. } => {} + _ => panic!("expected emit event effect"), } - total } #[cfg(feature = "action-refresh-fees")] - fn minted_effect_sum(effects: &[KernelEffect]) -> u128 { - let mut total = 0u128; - for effect in effects { - if let KernelEffect::MintShares { shares, .. } = effect { - total += *shares; - } + fn mint_shares_or_event_amount(effect: &KernelEffect) -> u128 { + match effect { + KernelEffect::MintShares { shares, .. } => *shares, + KernelEffect::EmitEvent { .. } => 0, + _ => panic!("refresh fees must not move assets or non-fee shares"), } - total } - fn payout_event(effects: &[KernelEffect]) -> Option<(bool, u128, u128, u128)> { - for effect in effects { - if let KernelEffect::EmitEvent { - event: - KernelEvent::PayoutCompleted { - success, - burn_shares, - refund_shares, - amount, - .. - }, - } = effect - { - return Some((*success, *burn_shares, *refund_shares, *amount)); - } + fn assert_refund_owner_is_owner(refund_owner: Option
) { + match refund_owner { + Some(owner) => assert_eq!(owner.0[0], OWNER.0[0]), + None => panic!("expected refund owner"), } - None } #[kani::proof] @@ -398,6 +376,65 @@ mod kani_proofs { assert_eq!(queue.head().map(|(id, _)| id), Some(second_id)); } + #[kani::proof] + #[kani::unwind(40)] + fn withdrawal_request_plan_preserves_accounting_and_enqueues_exact_escrow() { + let idle = bounded_amount(); + let external = bounded_amount(); + let total_shares = nonzero_bounded_amount(); + let shares = nonzero_bounded_amount(); + let expected_assets = bounded_amount(); + kani::assume(idle + external <= MAX_AMOUNT); + let config = zero_fee_config(); + let state = VaultState::with_initial( + idle + external, + total_shares, + idle, + external, + TimestampNs::ZERO, + ); + let before = state.clone(); + let plan = WithdrawalRequestPlan { + owner: RECEIVER, + receiver: OWNER, + shares, + expected_assets, + }; + + let requested = + apply_withdrawal_request_plan(state, &config, &SELF, plan, TimestampNs::ZERO).unwrap(); + + assert!(requested.state.op_state.is_idle()); + assert_eq!(requested.state.idle_assets, before.idle_assets); + assert_eq!(requested.state.external_assets, before.external_assets); + assert_eq!(requested.state.total_assets, before.total_assets); + assert_eq!(requested.state.total_shares, before.total_shares); + assert_eq!(requested.state.next_op_id, before.next_op_id); + assert_eq!(requested.state.withdraw_queue.status().length, 1); + assert_eq!( + requested.state.withdraw_queue.status().total_escrow_shares, + shares + ); + assert_eq!( + requested + .state + .withdraw_queue + .status() + .total_expected_assets, + expected_assets + ); + let (request_id, head) = requested.state.withdraw_queue.head().unwrap(); + assert_eq!(request_id, 0); + assert_address_eq(head.owner, RECEIVER); + assert_address_eq(head.receiver, OWNER); + assert_eq!(head.escrow_shares, shares); + assert_eq!(head.expected_assets, expected_assets); + assert_eq!(requested.effects.len(), 2); + assert_transfer_shares_effect(&requested.effects[0], RECEIVER, SELF, shares); + assert_emit_event_effect(&requested.effects[1]); + assert_asset_sum(&requested.state); + } + #[cfg(feature = "action-sync-external")] #[kani::proof] fn rebalance_withdraw_conserves_total_assets_and_moves_external_to_idle() { @@ -710,98 +747,6 @@ mod kani_proofs { assert!(state == baseline); } - #[cfg(all(feature = "action-recovery", feature = "kani-expensive-vault-proofs"))] - #[kani::proof] - #[kani::unwind(40)] - fn abort_withdrawing_requires_fifo_head_identity_and_refunds_escrow() { - let idle = bounded_amount(); - let external = bounded_amount(); - let total_shares = nonzero_bounded_amount(); - let first_shares = nonzero_bounded_amount(); - let second_shares = nonzero_bounded_amount(); - let first_expected = nonzero_bounded_amount(); - let second_expected = nonzero_bounded_amount(); - let collected = bounded_amount(); - - let mut state = VaultState::with_initial( - idle + external, - total_shares, - idle, - external, - TimestampNs::ZERO, - ); - let first_id = enqueue_withdrawal( - &mut state, - OWNER, - RECEIVER, - first_shares, - first_expected, - TimestampNs::ZERO, - ); - let second_id = enqueue_withdrawal( - &mut state, - SECOND_OWNER, - SECOND_RECEIVER, - second_shares, - second_expected, - TimestampNs::ZERO, - ); - - let op_id = 21; - let mismatched = WithdrawingState { - op_id, - request_id: second_id, - index: 0, - remaining: second_expected, - collected, - receiver: SECOND_RECEIVER, - owner: SECOND_OWNER, - escrow_shares: second_shares, - }; - let mut mismatch_state = state.clone(); - mismatch_state.op_state = OpState::Withdrawing(mismatched); - assert!(apply_action( - mismatch_state, - &zero_fee_config(), - None, - &SELF, - KernelAction::abort_withdrawing(op_id), - ) - .is_err()); - - let mut valid_state = state.clone(); - valid_state.op_state = OpState::Withdrawing(WithdrawingState { - op_id, - request_id: first_id, - index: 0, - remaining: first_expected, - collected, - receiver: RECEIVER, - owner: OWNER, - escrow_shares: first_shares, - }); - let result = apply_action( - valid_state, - &zero_fee_config(), - None, - &SELF, - KernelAction::abort_withdrawing(op_id), - ) - .unwrap(); - - assert!(result.state.op_state.is_idle()); - assert_asset_sum(&result.state); - assert_eq!(result.state.idle_assets, idle + collected); - assert_eq!(result.state.external_assets, external); - assert_eq!(result.state.total_shares, total_shares); - assert_eq!(refund_effect_sum(&result.effects, OWNER), first_shares); - assert_eq!(result.state.withdraw_queue.status().length, 1); - assert_eq!( - result.state.withdraw_queue.head().map(|(id, _)| id), - Some(second_id) - ); - } - #[kani::proof] fn withdrawal_collection_preserves_collected_plus_remaining() { let amount = nonzero_bounded_amount(); @@ -844,16 +789,144 @@ mod kani_proofs { assert!(payout.burn_shares <= payout.escrow_shares); } - #[cfg(feature = "kani-expensive-vault-proofs")] - fn payout_state( - idle: u128, - external: u128, - total_shares: u128, - escrow_shares: u128, - burn_shares: u128, - amount: u128, - op_id: u64, - ) -> VaultState { + #[kani::proof] + #[kani::unwind(40)] + fn withdrawal_queue_head_validation_requires_exact_identity_fields() { + let mut state = VaultState::with_initial(16, 16, 16, 0, TimestampNs::ZERO); + let first_id = enqueue_withdrawal(&mut state, OWNER, RECEIVER, 3, 5, TimestampNs::ZERO); + + assert!( + validate_queue_head(&state.withdraw_queue, first_id, &OWNER, &RECEIVER, 3,).is_ok() + ); + assert!( + validate_queue_head(&state.withdraw_queue, first_id + 1, &OWNER, &RECEIVER, 3,) + .is_err() + ); + assert!( + validate_queue_head(&state.withdraw_queue, first_id, &SECOND_OWNER, &RECEIVER, 3,) + .is_err() + ); + assert!( + validate_queue_head(&state.withdraw_queue, first_id, &OWNER, &SECOND_RECEIVER, 3,) + .is_err() + ); + assert!( + validate_queue_head(&state.withdraw_queue, first_id, &OWNER, &RECEIVER, 4,).is_err() + ); + assert_eq!( + state.withdraw_queue.head().map(|(id, _)| id), + Some(first_id) + ); + } + + #[kani::proof] + #[kani::unwind(40)] + fn withdrawal_queue_head_validation_rejects_later_fifo_entry() { + let mut state = VaultState::with_initial(16, 16, 16, 0, TimestampNs::ZERO); + let first_id = enqueue_withdrawal(&mut state, OWNER, RECEIVER, 3, 5, TimestampNs::ZERO); + let second_id = enqueue_withdrawal( + &mut state, + SECOND_OWNER, + SECOND_RECEIVER, + 7, + 11, + TimestampNs::ZERO, + ); + let before = state.withdraw_queue.status(); + + assert!( + validate_queue_head(&state.withdraw_queue, first_id, &OWNER, &RECEIVER, 3,).is_ok() + ); + assert!(validate_queue_head( + &state.withdraw_queue, + second_id, + &SECOND_OWNER, + &SECOND_RECEIVER, + 7, + ) + .is_err()); + assert_eq!( + state.withdraw_queue.head().map(|(id, _)| id), + Some(first_id) + ); + assert_eq!(state.withdraw_queue.status().length, before.length); + assert_eq!( + state.withdraw_queue.status().total_escrow_shares, + before.total_escrow_shares + ); + assert_eq!( + state.withdraw_queue.status().total_expected_assets, + before.total_expected_assets + ); + } + + #[kani::proof] + #[kani::unwind(40)] + fn withdrawal_fifo_head_maps_to_started_withdrawal_request() { + let mut state = VaultState::with_initial(16, 16, 16, 0, TimestampNs::ZERO); + let first_id = enqueue_withdrawal(&mut state, OWNER, RECEIVER, 3, 5, TimestampNs::ZERO); + + let head = pending_withdrawal_head(&state).unwrap(); + assert_eq!(head.id, first_id); + assert_address_eq(head.owner, OWNER); + assert_address_eq(head.receiver, RECEIVER); + assert_eq!(head.escrow_shares, 3); + assert_eq!(head.expected_assets, 5); + + let request = withdrawal_request_from_head(&mut state, head); + assert_eq!(request.request_id, first_id); + assert_address_eq(request.owner, OWNER); + assert_address_eq(request.receiver, RECEIVER); + assert_eq!(request.escrow_shares, 3); + assert_eq!(request.amount, 5); + assert_eq!(state.withdraw_queue.status().length, 1); + + let started = start_withdrawal(OpState::Idle, request).unwrap().new_state; + let withdrawing = started.as_withdrawing().unwrap(); + assert_eq!(withdrawing.request_id, first_id); + assert_address_eq(withdrawing.owner, OWNER); + assert_address_eq(withdrawing.receiver, RECEIVER); + assert_eq!(withdrawing.escrow_shares, 3); + assert_eq!(withdrawing.remaining, 5); + } + + #[kani::proof] + #[kani::unwind(40)] + fn payout_queue_head_dequeues_once_before_settlement() { + let mut queue = WithdrawQueue::new(); + let first_id = queue + .enqueue(OWNER, RECEIVER, 3, 5, TimestampNs::ZERO, 3) + .unwrap(); + let second_id = queue + .enqueue(SECOND_OWNER, SECOND_RECEIVER, 7, 11, TimestampNs::ZERO, 3) + .unwrap(); + + let (dequeued_id, dequeued) = queue.dequeue().unwrap(); + assert_eq!(dequeued_id, first_id); + assert_address_eq(dequeued.owner, OWNER); + assert_address_eq(dequeued.receiver, RECEIVER); + assert_eq!(dequeued.escrow_shares, 3); + assert_eq!(dequeued.expected_assets, 5); + assert_eq!(queue.status().length, 1); + assert_eq!(queue.status().total_escrow_shares, 7); + assert_eq!(queue.status().total_expected_assets, 11); + assert_eq!(queue.head().map(|(id, _)| id), Some(second_id)); + } + + #[kani::proof] + #[kani::unwind(40)] + fn payout_success_settlement_conserves_assets_and_escrow() { + let idle = nonzero_bounded_amount(); + let external = bounded_amount(); + let total_shares = nonzero_bounded_amount(); + let escrow_shares = nonzero_bounded_amount(); + let burn_shares = bounded_amount(); + let amount = bounded_amount(); + kani::assume(burn_shares <= escrow_shares); + kani::assume(burn_shares <= total_shares); + kani::assume(amount <= idle); + + let op_id = 41; let mut state = VaultState::with_initial( idle + external, total_shares, @@ -869,7 +942,7 @@ mod kani_proofs { amount, TimestampNs::ZERO, ); - state.op_state = OpState::Payout(PayoutState { + let payout = PayoutState { op_id, request_id, receiver: RECEIVER, @@ -877,14 +950,48 @@ mod kani_proofs { owner: OWNER, escrow_shares, burn_shares, - }); - state + }; + + assert!(validate_queue_head( + &state.withdraw_queue, + payout.request_id, + &payout.owner, + &payout.receiver, + payout.escrow_shares, + ) + .is_ok()); + let (dequeued_id, dequeued) = state.withdraw_queue.dequeue().unwrap(); + assert_eq!(dequeued_id, request_id); + assert_address_eq(dequeued.owner, OWNER); + assert_address_eq(dequeued.receiver, RECEIVER); + assert_eq!(dequeued.escrow_shares, escrow_shares); + assert_eq!(state.withdraw_queue.status().length, 0); + + let settlement = plan_payout_settlement(&payout, PayoutOutcome::Success).unwrap(); + let mut effects = Vec::new(); + apply_payout_settlement(&mut state, &payout, settlement, SELF, &mut effects).unwrap(); + + assert!(state.op_state.is_idle()); + assert_asset_sum(&state); + assert!(settlement.success); + assert_eq!(settlement.burn_shares, burn_shares); + assert_eq!(settlement.refund_shares, escrow_shares - burn_shares); + assert_eq!( + settlement.burn_shares + settlement.refund_shares, + escrow_shares + ); + assert_eq!(settlement.completed_amount, amount); + assert_eq!(state.idle_assets, idle - amount); + assert_eq!(state.external_assets, external); + assert_eq!(state.total_assets, idle + external - amount); + assert_eq!(state.total_shares, total_shares - burn_shares); + assert_eq!(state.withdraw_queue.status().length, 0); } - #[cfg(feature = "kani-expensive-vault-proofs")] #[kani::proof] #[kani::unwind(40)] - fn payout_success_settlement_conserves_assets_and_escrow() { + fn payout_failure_settlement_refunds_without_mutating_assets_or_shares_and_dequeues_head_once() + { let idle = nonzero_bounded_amount(); let external = bounded_amount(); let total_shares = nonzero_bounded_amount(); @@ -892,239 +999,261 @@ mod kani_proofs { let burn_shares = bounded_amount(); let amount = bounded_amount(); kani::assume(burn_shares <= escrow_shares); - kani::assume(burn_shares <= total_shares); kani::assume(amount <= idle); - let op_id = 41; - let success = apply_action( - payout_state( - idle, - external, - total_shares, - escrow_shares, - burn_shares, - amount, - op_id, - ), - &zero_fee_config(), - None, - &SELF, - KernelAction::settle_payout(op_id, PayoutOutcome::Success), - ) - .unwrap(); - assert!(success.state.op_state.is_idle()); - assert_asset_sum(&success.state); - assert_eq!(success.state.idle_assets, idle - amount); - assert_eq!(success.state.external_assets, external); - assert_eq!(success.state.total_assets, idle + external - amount); - assert_eq!(success.state.total_shares, total_shares - burn_shares); - assert_eq!(success.state.withdraw_queue.status().length, 0); - assert_eq!(burn_effect_sum(&success.effects), burn_shares); - assert_eq!( - refund_effect_sum(&success.effects, OWNER), - escrow_shares - burn_shares + let op_id = 42; + let mut state = VaultState::with_initial( + idle + external, + total_shares, + idle, + external, + TimestampNs::ZERO, ); - assert_eq!( - payout_event(&success.effects), - Some((true, burn_shares, escrow_shares - burn_shares, amount)) + let request_id = enqueue_withdrawal( + &mut state, + OWNER, + RECEIVER, + escrow_shares, + amount, + TimestampNs::ZERO, ); + let payout = PayoutState { + op_id, + request_id, + receiver: RECEIVER, + amount, + owner: OWNER, + escrow_shares, + burn_shares, + }; + + assert!(validate_queue_head( + &state.withdraw_queue, + payout.request_id, + &payout.owner, + &payout.receiver, + payout.escrow_shares, + ) + .is_ok()); + let (dequeued_id, dequeued) = state.withdraw_queue.dequeue().unwrap(); + assert_eq!(dequeued_id, request_id); + assert_address_eq(dequeued.owner, OWNER); + assert_address_eq(dequeued.receiver, RECEIVER); + assert_eq!(dequeued.escrow_shares, escrow_shares); + assert_eq!(state.withdraw_queue.status().length, 0); + + let settlement = plan_payout_settlement(&payout, PayoutOutcome::Failure).unwrap(); + let mut effects = Vec::new(); + apply_payout_settlement(&mut state, &payout, settlement, SELF, &mut effects).unwrap(); + + assert!(state.op_state.is_idle()); + assert_asset_sum(&state); + assert!(!settlement.success); + assert_eq!(settlement.burn_shares, 0); + assert_eq!(settlement.refund_shares, escrow_shares); + assert_eq!(settlement.completed_amount, 0); + assert_eq!(state.idle_assets, idle); + assert_eq!(state.external_assets, external); + assert_eq!(state.total_assets, idle + external); + assert_eq!(state.total_shares, total_shares); } - #[cfg(feature = "kani-expensive-vault-proofs")] + #[cfg(feature = "action-recovery")] #[kani::proof] - #[kani::unwind(40)] - fn payout_failure_settlement_refunds_without_mutating_assets_or_shares() { - let idle = nonzero_bounded_amount(); + #[kani::unwind(8)] + fn emergency_reset_allocating_restores_remaining_assets_to_idle() { + let idle = bounded_amount(); let external = bounded_amount(); - let total_shares = nonzero_bounded_amount(); - let escrow_shares = nonzero_bounded_amount(); - let burn_shares = bounded_amount(); - let amount = bounded_amount(); - kani::assume(burn_shares <= escrow_shares); - kani::assume(burn_shares <= total_shares); - kani::assume(amount <= idle); + let total_shares = bounded_amount(); + let remaining = bounded_amount(); + let op_id = 51; - let op_id = 42; - let failure = apply_action( - payout_state( - idle, - external, - total_shares, - escrow_shares, - burn_shares, - amount, - op_id, - ), - &zero_fee_config(), - None, - &SELF, - KernelAction::settle_payout(op_id, PayoutOutcome::Failure), - ) - .unwrap(); - assert!(failure.state.op_state.is_idle()); - assert_asset_sum(&failure.state); - assert_eq!(failure.state.idle_assets, idle); - assert_eq!(failure.state.external_assets, external); - assert_eq!(failure.state.total_assets, idle + external); - assert_eq!(failure.state.total_shares, total_shares); - assert_eq!(failure.state.withdraw_queue.status().length, 0); - assert_eq!(burn_effect_sum(&failure.effects), 0); - assert_eq!(refund_effect_sum(&failure.effects, OWNER), escrow_shares); + let mut state = VaultState::with_initial( + idle + external, + total_shares, + idle, + external, + TimestampNs::ZERO, + ); + state.op_state = OpState::Allocating(AllocatingState { + op_id, + index: 0, + remaining, + plan: allocation_plan(remaining, 0), + }); + + let result = plan_emergency_reset(state).unwrap(); + + assert!(result.state.op_state.is_idle()); + assert_eq!(result.state.idle_assets, idle + remaining); + assert_eq!(result.state.external_assets, external); + assert_eq!(result.state.total_assets, idle + external + remaining); + assert_eq!(result.state.total_shares, total_shares); + assert_eq!(result.state.withdraw_queue.status().length, 0); + assert!(result.refund_owner.is_none()); + assert_eq!(result.refund_shares, 0); assert_eq!( - payout_event(&failure.effects), - Some((false, 0, escrow_shares, 0)) + result.state.fee_anchor.total_assets, + result.state.total_assets ); + assert_asset_sum(&result.state); } - #[cfg(all(feature = "action-recovery", feature = "kani-expensive-vault-proofs"))] + #[cfg(feature = "action-recovery")] #[kani::proof] - #[kani::unwind(40)] - fn emergency_reset_recovers_non_idle_states_without_share_or_queue_leakage() { + #[kani::unwind(8)] + fn emergency_reset_withdrawing_restores_collected_assets_and_refunds_escrow() { let idle = bounded_amount(); let external = bounded_amount(); - let shares = nonzero_bounded_amount(); - let amount = bounded_amount(); - let escrow = nonzero_bounded_amount(); - let kind = kani::any::(); - kani::assume(kind < 4); + let total_shares = nonzero_bounded_amount(); + let remaining = bounded_amount(); + let collected = bounded_amount(); + let escrow_shares = nonzero_bounded_amount(); + let op_id = 52; - let mut state = - VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); - let op_id = 51; - let expected_idle_restore; - let expected_refund; - let expected_queue_len; + let mut state = VaultState::with_initial( + idle + external, + total_shares, + idle, + external, + TimestampNs::ZERO, + ); + state.op_state = OpState::Withdrawing(WithdrawingState { + op_id, + request_id: 0, + index: 0, + remaining, + collected, + receiver: RECEIVER, + owner: OWNER, + escrow_shares, + }); - if kind == 0 { - state.op_state = OpState::Allocating(AllocatingState { - op_id, - index: 0, - remaining: amount, - plan: allocation_plan(amount, 0), - }); - expected_idle_restore = amount; - expected_refund = 0; - expected_queue_len = 0; - } else if kind == 1 { - let request_id = enqueue_withdrawal( - &mut state, - OWNER, - RECEIVER, - escrow, - amount, - TimestampNs::ZERO, - ); - state.op_state = OpState::Withdrawing(WithdrawingState { - op_id, - request_id, - index: 0, - remaining: amount, - collected: amount, - receiver: RECEIVER, - owner: OWNER, - escrow_shares: escrow, - }); - expected_idle_restore = amount; - expected_refund = escrow; - expected_queue_len = 0; - } else if kind == 2 { - let request_id = enqueue_withdrawal( - &mut state, - OWNER, - RECEIVER, - escrow, - amount, - TimestampNs::ZERO, - ); - state.op_state = OpState::Payout(PayoutState { - op_id, - request_id, - receiver: RECEIVER, - amount, - owner: OWNER, - escrow_shares: escrow, - burn_shares: 0, - }); - expected_idle_restore = amount; - expected_refund = escrow; - expected_queue_len = 0; - } else { - state.op_state = OpState::Refreshing(RefreshingState { - op_id, - index: 0, - plan: vec![0], - }); - expected_idle_restore = 0; - expected_refund = 0; - expected_queue_len = 0; - } - - let result = apply_action( - state, - &zero_fee_config(), - None, - &SELF, - KernelAction::emergency_reset(), - ) - .unwrap(); + let result = plan_emergency_reset(state).unwrap(); assert!(result.state.op_state.is_idle()); + assert_eq!(result.state.idle_assets, idle + collected); + assert_eq!(result.state.external_assets, external); + assert_eq!(result.state.total_assets, idle + external + collected); + assert_eq!(result.state.total_shares, total_shares); + assert_eq!(result.state.withdraw_queue.status().length, 0); + assert_refund_owner_is_owner(result.refund_owner); + assert_eq!(result.refund_shares, escrow_shares); + assert_eq!( + result.state.fee_anchor.total_assets, + result.state.total_assets + ); assert_asset_sum(&result.state); - assert_eq!(result.state.idle_assets, idle + expected_idle_restore); + } + + #[cfg(feature = "action-recovery")] + #[kani::proof] + #[kani::unwind(8)] + fn emergency_reset_payout_restores_payout_assets_and_refunds_escrow() { + let idle = bounded_amount(); + let external = bounded_amount(); + let total_shares = nonzero_bounded_amount(); + let amount = bounded_amount(); + let escrow_shares = nonzero_bounded_amount(); + let burn_shares = bounded_amount(); + let op_id = 53; + kani::assume(burn_shares <= escrow_shares); + + let mut state = VaultState::with_initial( + idle + external, + total_shares, + idle, + external, + TimestampNs::ZERO, + ); + state.op_state = OpState::Payout(PayoutState { + op_id, + request_id: 0, + receiver: RECEIVER, + amount, + owner: OWNER, + escrow_shares, + burn_shares, + }); + + let result = plan_emergency_reset(state).unwrap(); + + assert!(result.state.op_state.is_idle()); + assert_eq!(result.state.idle_assets, idle + amount); assert_eq!(result.state.external_assets, external); - assert_eq!(result.state.total_shares, shares); + assert_eq!(result.state.total_assets, idle + external + amount); + assert_eq!(result.state.total_shares, total_shares); + assert_eq!(result.state.withdraw_queue.status().length, 0); + assert_refund_owner_is_owner(result.refund_owner); + assert_eq!(result.refund_shares, escrow_shares); + assert_eq!( + result.state.fee_anchor.total_assets, + result.state.total_assets + ); + assert_asset_sum(&result.state); + } + + #[cfg(feature = "action-recovery")] + #[kani::proof] + #[kani::unwind(8)] + fn emergency_reset_refreshing_returns_idle_without_accounting_mutation() { + let idle = bounded_amount(); + let external = bounded_amount(); + let total_shares = bounded_amount(); + let op_id = 54; + + let mut state = VaultState::with_initial( + idle + external, + total_shares, + idle, + external, + TimestampNs::ZERO, + ); + let before = state.clone(); + state.op_state = OpState::Refreshing(RefreshingState { + op_id, + index: 1, + plan: vec![7, 8], + }); + + let result = plan_emergency_reset(state).unwrap(); + + assert!(result.state.op_state.is_idle()); + assert_eq!(result.state.idle_assets, before.idle_assets); + assert_eq!(result.state.external_assets, before.external_assets); + assert_eq!(result.state.total_assets, before.total_assets); + assert_eq!(result.state.total_shares, before.total_shares); assert_eq!( result.state.withdraw_queue.status().length, - expected_queue_len + before.withdraw_queue.status().length ); - assert_eq!(refund_effect_sum(&result.effects, OWNER), expected_refund); + assert!(result.refund_owner.is_none()); + assert_eq!(result.refund_shares, 0); assert_eq!( result.state.fee_anchor.total_assets, result.state.total_assets ); + assert_asset_sum(&result.state); } #[cfg(feature = "action-sync-external")] #[kani::proof] - #[kani::unwind(40)] - fn sync_external_assets_only_mutates_external_and_total_assets_for_allowed_ops() { + #[kani::unwind(8)] + fn sync_external_assets_allocating_only_mutates_external_and_total_assets() { let idle = bounded_amount(); let external = bounded_amount(); let synced_external = bounded_amount(); let shares = bounded_amount(); - let op_kind = kani::any::(); - kani::assume(op_kind < 3); + let op_id = 61; let mut state = VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); - let op_id = 61; - if op_kind == 0 { - state.op_state = OpState::Allocating(AllocatingState { - op_id, - index: 1, - remaining: 2, - plan: allocation_plan(1, 1), - }); - } else if op_kind == 1 { - let request_id = - enqueue_withdrawal(&mut state, OWNER, RECEIVER, 3, 4, TimestampNs::ZERO); - state.op_state = OpState::Withdrawing(WithdrawingState { - op_id, - request_id, - index: 1, - remaining: 2, - collected: 2, - receiver: RECEIVER, - owner: OWNER, - escrow_shares: 3, - }); - } else { - state.op_state = OpState::Refreshing(RefreshingState { - op_id, - index: 1, - plan: vec![7, 8], - }); - } + state.op_state = OpState::Allocating(AllocatingState { + op_id, + index: 1, + remaining: 2, + plan: allocation_plan(1, 1), + }); let before_idle = state.idle_assets; let before_shares = state.total_shares; @@ -1163,39 +1292,166 @@ mod kani_proofs { before_fee_anchor_total_assets ); assert!(result.state.fee_anchor.timestamp_ns == before_fee_anchor_timestamp); - match &result.state.op_state { - OpState::Allocating(alloc) => { - assert_eq!(op_kind, 0); - assert_eq!(alloc.op_id, op_id); - assert_eq!(alloc.index, 1); - assert_eq!(alloc.remaining, 2); - } - OpState::Withdrawing(withdraw) => { - assert_eq!(op_kind, 1); - assert_eq!(withdraw.op_id, op_id); - assert_eq!(withdraw.index, 1); - assert_eq!(withdraw.remaining, 2); - assert_eq!(withdraw.collected, 2); - assert_address_eq(withdraw.owner, OWNER); - assert_address_eq(withdraw.receiver, RECEIVER); - assert_eq!(withdraw.escrow_shares, 3); - } - OpState::Refreshing(refresh) => { - assert_eq!(op_kind, 2); - assert_eq!(refresh.op_id, op_id); - assert_eq!(refresh.index, 1); - } - _ => panic!("sync must preserve active operation kind"), + if let OpState::Allocating(alloc) = &result.state.op_state { + assert_eq!(alloc.op_id, op_id); + assert_eq!(alloc.index, 1); + assert_eq!(alloc.remaining, 2); + } else { + panic!("sync must preserve allocating operation"); } assert_asset_sum(&result.state); + } - let idle_state = VaultState::with_initial( - before_idle + synced_external, - before_shares, - before_idle, - synced_external, - TimestampNs::ZERO, + #[cfg(feature = "action-sync-external")] + #[kani::proof] + #[kani::unwind(8)] + fn sync_external_assets_withdrawing_preserves_share_supply_queue_and_actor_fields() { + let idle = bounded_amount(); + let external = bounded_amount(); + let synced_external = bounded_amount(); + let shares = bounded_amount(); + let op_id = 62; + + let mut state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + state.op_state = OpState::Withdrawing(WithdrawingState { + op_id, + request_id: 7, + index: 1, + remaining: 2, + collected: 2, + receiver: RECEIVER, + owner: OWNER, + escrow_shares: 3, + }); + + let before_queue = state.withdraw_queue.status(); + let before_next_op_id = state.next_op_id; + let result = apply_action( + state, + &zero_fee_config(), + None, + &SELF, + KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO), + ) + .unwrap(); + + assert_eq!(result.state.idle_assets, idle); + assert_eq!(result.state.external_assets, synced_external); + assert_eq!(result.state.total_assets, idle + synced_external); + assert_eq!(result.state.total_shares, shares); + assert_eq!( + result.state.withdraw_queue.status().length, + before_queue.length + ); + assert_eq!( + result.state.withdraw_queue.status().total_escrow_shares, + before_queue.total_escrow_shares + ); + assert_eq!( + result.state.withdraw_queue.status().total_expected_assets, + before_queue.total_expected_assets ); + assert_eq!(result.state.next_op_id, before_next_op_id); + if let OpState::Withdrawing(withdraw) = &result.state.op_state { + assert_eq!(withdraw.op_id, op_id); + assert_eq!(withdraw.request_id, 7); + assert_eq!(withdraw.index, 1); + assert_eq!(withdraw.remaining, 2); + assert_eq!(withdraw.collected, 2); + assert_eq!(withdraw.owner.0[0], OWNER.0[0]); + assert_eq!(withdraw.receiver.0[0], RECEIVER.0[0]); + assert_eq!(withdraw.escrow_shares, 3); + } else { + panic!("sync must preserve withdrawing operation"); + } + assert_asset_sum(&result.state); + } + + #[cfg(feature = "action-sync-external")] + #[kani::proof] + #[kani::unwind(8)] + fn sync_external_assets_refreshing_only_mutates_external_and_total_assets() { + let idle = bounded_amount(); + let external = bounded_amount(); + let synced_external = bounded_amount(); + let shares = bounded_amount(); + let op_id = 63; + + let mut state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + state.op_state = OpState::Refreshing(RefreshingState { + op_id, + index: 1, + plan: vec![7, 8], + }); + + let before_queue = state.withdraw_queue.status(); + let before_next_op_id = state.next_op_id; + let result = apply_action( + state, + &zero_fee_config(), + None, + &SELF, + KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO), + ) + .unwrap(); + + assert_eq!(result.state.idle_assets, idle); + assert_eq!(result.state.external_assets, synced_external); + assert_eq!(result.state.total_assets, idle + synced_external); + assert_eq!(result.state.total_shares, shares); + assert_eq!( + result.state.withdraw_queue.status().length, + before_queue.length + ); + assert_eq!( + result.state.withdraw_queue.status().total_escrow_shares, + before_queue.total_escrow_shares + ); + assert_eq!( + result.state.withdraw_queue.status().total_expected_assets, + before_queue.total_expected_assets + ); + assert_eq!(result.state.next_op_id, before_next_op_id); + if let OpState::Refreshing(refresh) = &result.state.op_state { + assert_eq!(refresh.op_id, op_id); + assert_eq!(refresh.index, 1); + } else { + panic!("sync must preserve refreshing operation"); + } + assert_asset_sum(&result.state); + } + + #[cfg(feature = "action-sync-external")] + #[kani::proof] + #[kani::unwind(8)] + fn sync_external_assets_rejects_wrong_op_id_and_disallowed_states() { + let idle = bounded_amount(); + let external = bounded_amount(); + let synced_external = bounded_amount(); + let shares = bounded_amount(); + let op_id = 64; + + let mut allocating = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + allocating.op_state = OpState::Allocating(AllocatingState { + op_id, + index: 1, + remaining: 2, + plan: allocation_plan(1, 1), + }); + assert!(apply_action( + allocating, + &zero_fee_config(), + None, + &SELF, + KernelAction::sync_external_assets(synced_external, op_id + 1, TimestampNs::ZERO), + ) + .is_err()); + + let idle_state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); assert!(apply_action( idle_state, &zero_fee_config(), @@ -1204,6 +1460,26 @@ mod kani_proofs { KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO), ) .is_err()); + + let mut payout_state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + payout_state.op_state = OpState::Payout(PayoutState { + op_id, + request_id: 0, + receiver: RECEIVER, + amount: 1, + owner: OWNER, + escrow_shares: 1, + burn_shares: 1, + }); + assert!(apply_action( + payout_state, + &zero_fee_config(), + None, + &SELF, + KernelAction::sync_external_assets(synced_external, op_id, TimestampNs::ZERO), + ) + .is_err()); } #[cfg(all(feature = "action-refresh-lifecycle", feature = "action-sync-external"))] @@ -1285,11 +1561,11 @@ mod kani_proofs { ) .unwrap(); - let minted = minted_effect_sum(&result.effects); assert_eq!(result.state.idle_assets, before.idle_assets); assert_eq!(result.state.external_assets, before.external_assets); assert_eq!(result.state.total_assets, before.total_assets); - assert_eq!(minted, 0); + assert_eq!(result.effects.len(), 1); + assert_emit_event_effect(&result.effects[0]); assert_eq!(result.state.total_shares, before.total_shares); assert_eq!( result.state.fee_anchor.total_assets, @@ -1313,6 +1589,70 @@ mod kani_proofs { assert_eq!(result.state.next_op_id, before.next_op_id); assert_asset_sum(&result.state); } + + #[cfg(feature = "action-refresh-fees")] + #[kani::proof] + #[kani::unwind(8)] + fn refresh_fees_active_rates_only_mint_fee_shares_and_update_anchor() { + let idle = 0u128; + let external = 0u128; + let shares = 0u128; + let anchor_assets = 0u128; + let now = TimestampNs::from_nanos(1); + + let mut state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + state.fee_anchor = FeeAccrualAnchor::new(anchor_assets, TimestampNs::ZERO); + let before = state.clone(); + let before_queue = before.withdraw_queue.status(); + + let result = apply_action( + state, + &active_fee_config(), + None, + &SELF, + KernelAction::refresh_fees(now), + ) + .unwrap(); + + let effect_count = result.effects.len(); + assert!(effect_count > 0); + assert!(effect_count <= 3); + let mut minted = mint_shares_or_event_amount(&result.effects[0]); + if effect_count > 1 { + minted += mint_shares_or_event_amount(&result.effects[1]); + } + if effect_count > 2 { + minted += mint_shares_or_event_amount(&result.effects[2]); + } + + assert_eq!(result.state.idle_assets, before.idle_assets); + assert_eq!(result.state.external_assets, before.external_assets); + assert_eq!(result.state.total_assets, before.total_assets); + assert!(result.state.total_shares >= before.total_shares); + assert_eq!(result.state.total_shares, before.total_shares + minted); + assert_eq!( + result.state.fee_anchor.total_assets, + result.state.total_assets + ); + assert!(result.state.fee_anchor.timestamp_ns == now); + assert!(result.state.fee_anchor.timestamp_ns > before.fee_anchor.timestamp_ns); + assert!(result.state.op_state.is_idle()); + assert_eq!( + result.state.withdraw_queue.status().length, + before_queue.length + ); + assert_eq!( + result.state.withdraw_queue.status().total_escrow_shares, + before_queue.total_escrow_shares + ); + assert_eq!( + result.state.withdraw_queue.status().total_expected_assets, + before_queue.total_expected_assets + ); + assert_eq!(result.state.next_op_id, before.next_op_id); + assert_asset_sum(&result.state); + } } pub use types::{ActualIdx, Address, AssetId, DurationNs, ExpectedIdx, KernelVersion, TimestampNs}; pub use utils::TimeGate; From 0408ab0d966f45102b0e3e8741350bd2c3292d10 Mon Sep 17 00:00:00 2001 From: carrion256 Date: Tue, 23 Jun 2026 17:32:26 +0200 Subject: [PATCH 06/11] ENG-162 tighten vault Kani invariants --- .github/workflows/kani.yml | 19 ++++++++ contract/vault/kernel/src/lib.rs | 74 +++++++++++++++++++++++++++++++- 2 files changed, 91 insertions(+), 2 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index b9d253e6c..8b90df165 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -88,6 +88,25 @@ jobs: --harness sync_external_assets_refreshing_only_mutates_external_and_total_assets --harness sync_external_assets_rejects_wrong_op_id_and_disallowed_states + vault-kernel-withdraw-escrow: + name: Vault Kernel / Withdraw Escrow + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - name: Checkout repository + uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 + with: + persist-credentials: false + + - name: Run Vault Kernel withdraw escrow Kani proof + uses: model-checking/kani-github-action@v1 + with: + kani-version: ${{ env.KANI_VERSION }} + command: cargo-kani + args: >- + -p templar-vault-kernel + --harness post_deposit_request_withdraw_preserves_accounting_and_escrows_previewed_shares + vault-kernel-allocation-lifecycle: name: Vault Kernel / Allocation Lifecycle runs-on: ubuntu-latest diff --git a/contract/vault/kernel/src/lib.rs b/contract/vault/kernel/src/lib.rs index aeceb8153..8180ca999 100644 --- a/contract/vault/kernel/src/lib.rs +++ b/contract/vault/kernel/src/lib.rs @@ -435,6 +435,75 @@ mod kani_proofs { assert_asset_sum(&requested.state); } + #[kani::proof] + #[kani::unwind(40)] + fn post_deposit_request_withdraw_preserves_accounting_and_escrows_previewed_shares() { + let deposited_assets = nonzero_bounded_amount(); + let minted_shares = deposited_assets; + let config = zero_fee_config(); + let post_deposit = VaultState::with_initial( + deposited_assets, + minted_shares, + deposited_assets, + 0, + TimestampNs::from_nanos(1), + ); + let post_deposit_idle_assets = post_deposit.idle_assets; + let post_deposit_external_assets = post_deposit.external_assets; + let post_deposit_total_assets = post_deposit.total_assets; + let post_deposit_total_shares = post_deposit.total_shares; + let post_deposit_next_op_id = post_deposit.next_op_id; + let expected_assets = deposited_assets; + let request_plan = WithdrawalRequestPlan { + owner: RECEIVER, + receiver: OWNER, + shares: minted_shares, + expected_assets, + }; + + let requested = apply_withdrawal_request_plan( + post_deposit, + &config, + &SELF, + request_plan, + TimestampNs::from_nanos(2), + ) + .unwrap(); + + assert!(requested.state.op_state.is_idle()); + assert_eq!(requested.state.idle_assets, post_deposit_idle_assets); + assert_eq!( + requested.state.external_assets, + post_deposit_external_assets + ); + assert_eq!(requested.state.total_assets, post_deposit_total_assets); + assert_eq!(requested.state.total_shares, post_deposit_total_shares); + assert_eq!(requested.state.next_op_id, post_deposit_next_op_id); + assert_eq!(requested.state.withdraw_queue.status().length, 1); + assert_eq!( + requested.state.withdraw_queue.status().total_escrow_shares, + minted_shares + ); + assert_eq!( + requested + .state + .withdraw_queue + .status() + .total_expected_assets, + expected_assets + ); + let (request_id, head) = requested.state.withdraw_queue.head().unwrap(); + assert_eq!(request_id, 0); + assert_address_eq(head.owner, RECEIVER); + assert_address_eq(head.receiver, OWNER); + assert_eq!(head.escrow_shares, minted_shares); + assert_eq!(head.expected_assets, expected_assets); + assert_eq!(requested.effects.len(), 2); + assert_transfer_shares_effect(&requested.effects[0], RECEIVER, SELF, minted_shares); + assert_emit_event_effect(&requested.effects[1]); + assert_asset_sum(&requested.state); + } + #[cfg(feature = "action-sync-external")] #[kani::proof] fn rebalance_withdraw_conserves_total_assets_and_moves_external_to_idle() { @@ -1594,9 +1663,9 @@ mod kani_proofs { #[kani::proof] #[kani::unwind(8)] fn refresh_fees_active_rates_only_mint_fee_shares_and_update_anchor() { - let idle = 0u128; + let idle = 100u128; let external = 0u128; - let shares = 0u128; + let shares = 100u128; let anchor_assets = 0u128; let now = TimestampNs::from_nanos(1); @@ -1626,6 +1695,7 @@ mod kani_proofs { minted += mint_shares_or_event_amount(&result.effects[2]); } + assert!(minted > 0); assert_eq!(result.state.idle_assets, before.idle_assets); assert_eq!(result.state.external_assets, before.external_assets); assert_eq!(result.state.total_assets, before.total_assets); From ed4a504b5c6437a206b7539e5ac7fc4fc7485e67 Mon Sep 17 00:00:00 2001 From: carrion256 Date: Tue, 23 Jun 2026 17:48:31 +0200 Subject: [PATCH 07/11] ENG-162 reduce refresh fee Kani proof cost --- contract/vault/kernel/src/lib.rs | 23 +++++++++-------------- 1 file changed, 9 insertions(+), 14 deletions(-) diff --git a/contract/vault/kernel/src/lib.rs b/contract/vault/kernel/src/lib.rs index 8180ca999..6662d9919 100644 --- a/contract/vault/kernel/src/lib.rs +++ b/contract/vault/kernel/src/lib.rs @@ -111,7 +111,7 @@ mod kani_proofs { VaultConfig { fees: FeesSpec::new( FeeSlot::new(Wad::one() / 10, Address([0x66; 32])), - FeeSlot::new(Wad::one() / 20, Address([0x77; 32])), + FeeSlot::zero(), None, ), min_withdrawal_assets: 0, @@ -198,10 +198,12 @@ mod kani_proofs { } #[cfg(feature = "action-refresh-fees")] - fn mint_shares_or_event_amount(effect: &KernelEffect) -> u128 { + fn assert_mint_shares_effect(effect: &KernelEffect) -> u128 { match effect { - KernelEffect::MintShares { shares, .. } => *shares, - KernelEffect::EmitEvent { .. } => 0, + KernelEffect::MintShares { shares, .. } => { + assert!(*shares > 0); + *shares + } _ => panic!("refresh fees must not move assets or non-fee shares"), } } @@ -1684,16 +1686,9 @@ mod kani_proofs { ) .unwrap(); - let effect_count = result.effects.len(); - assert!(effect_count > 0); - assert!(effect_count <= 3); - let mut minted = mint_shares_or_event_amount(&result.effects[0]); - if effect_count > 1 { - minted += mint_shares_or_event_amount(&result.effects[1]); - } - if effect_count > 2 { - minted += mint_shares_or_event_amount(&result.effects[2]); - } + assert_eq!(result.effects.len(), 2); + let minted = assert_mint_shares_effect(&result.effects[0]); + assert_emit_event_effect(&result.effects[1]); assert!(minted > 0); assert_eq!(result.state.idle_assets, before.idle_assets); From 2e257b9cd484c9f6c4777e33c3d7b6410e2e7e93 Mon Sep 17 00:00:00 2001 From: carrion256 Date: Tue, 23 Jun 2026 18:02:16 +0200 Subject: [PATCH 08/11] ENG-162 update Soroban vault CLI operator docs --- tools/soroban-vault-cli/README.md | 68 +++++++++++++++++++++++++------ 1 file changed, 56 insertions(+), 12 deletions(-) diff --git a/tools/soroban-vault-cli/README.md b/tools/soroban-vault-cli/README.md index bd35f2532..420ca9710 100644 --- a/tools/soroban-vault-cli/README.md +++ b/tools/soroban-vault-cli/README.md @@ -143,8 +143,8 @@ Common role terms: run market allocation and refresh operations. The vault curator is always authorized as an allocator too. - `adapter`: a market route such as a Blend adapter or custodial adapter. The governance admin must - allow adapters and place them into the typed supply queue before allocations can route through - them. + allow adapters, set a nonzero market cap, and place them into the typed supply queue before + allocations can route through them. ### Allocation Through Adapters @@ -156,13 +156,22 @@ Allocation is a two-step mental model: Adapters can exist in the deployment manifest before they are usable by the vault. A Blend or custodial adapter becomes an active supply route only after governance adds it to the allowed -adapter set and binds it into the supply queue: +adapter set, sets a nonzero market cap, and binds it into the supply queue: ```sh tmplr-soroban-vault governance submit-set-allowed-adapters \ --admin GCURATOR_OR_MULTISIG... \ --adapters CBLENDADAPTER...,CCUSTODIALADAPTER... +tmplr-soroban-vault governance submit-set-cap \ + --admin GCURATOR_OR_MULTISIG... \ + --market-id 0 \ + --cap 1000000000 +tmplr-soroban-vault governance submit-set-cap \ + --admin GCURATOR_OR_MULTISIG... \ + --market-id 1 \ + --cap 1000000000 + tmplr-soroban-vault governance submit-set-supply-queue \ --admin GCURATOR_OR_MULTISIG... \ --entry 0:CBLENDADAPTER... \ @@ -196,8 +205,9 @@ For cross-chain Templar market routes, keep the accounting boundary at the adapt not track each off-chain hop after assets leave Stellar, and it does not map individual vault shares to a NEAR account, universal account, or market position. User shares are derived from vault NAV: `total_assets / total_shares`. The adapter reports the aggregate route NAV back to the vault through -its `total_assets(asset)` surface, and the vault incorporates that value when allocators supply, -withdraw, or run `curator refresh-markets`. +its `total_assets(asset)` surface, and the vault incorporates that value when allocators supply or +run `curator refresh-markets`. `curator allocate-withdraw` does not refresh route NAV; it verifies +the realized token balance delta and subtracts that amount from stored principal. Operationally, a Templar route may move assets through custody, bridge or intents infrastructure, and a NEAR-side supply position. From the Stellar vault's perspective, that path is one @@ -209,7 +219,7 @@ Withdrawals use two different CLI surfaces: - `curator allocate-withdraw` is an allocator operation. It pulls liquidity back from the adapter bound to a market id by calling the adapter's `progress_withdrawal(vault, asset, amount)`. The `amount` is the requested adapter withdrawal amount; the vault accounts the assets actually - returned by the adapter. + returned by the adapter without calling adapter `total_assets`. - `user request-withdraw` and `user execute-withdraw` are user exit operations. `request-withdraw` queues shares for withdrawal after the configured cooldown. `execute-withdraw` attempts to pay the next ready request from idle vault assets. If idle assets are not sufficient, an allocator first @@ -269,6 +279,12 @@ tmplr-soroban-vault governance submit-set-allowed-adapters \ --adapters CBLENDADAPTER... tmplr-soroban-vault governance accept-ready --admin GCURATOR... --kind allowed-adapters +tmplr-soroban-vault governance submit-set-cap \ + --admin GCURATOR... \ + --market-id 0 \ + --cap 1000000000 +tmplr-soroban-vault governance accept-ready --admin GCURATOR... --kind cap + tmplr-soroban-vault governance submit-set-supply-queue \ --admin GCURATOR... \ --entry 0:CBLENDADAPTER... @@ -289,6 +305,11 @@ tmplr-soroban-vault curator set-allowed-adapters \ --admin GCURATOR... \ --adapters CBLENDADAPTER... \ --auto-accept +tmplr-soroban-vault governance submit-set-cap \ + --admin GCURATOR... \ + --market-id 0 \ + --cap 1000000000 +tmplr-soroban-vault governance accept-ready --admin GCURATOR... --kind cap tmplr-soroban-vault curator set-supply-queue \ --admin GCURATOR... \ --entry 0:CBLENDADAPTER... \ @@ -312,6 +333,9 @@ tmplr-soroban-vault governance plan-submit-set-supply-queue \ --entry 0:CBLENDADAPTER... ``` +Fresh markets need an accepted `submit-set-cap --market-id ... --cap ...` proposal before governance +accepts a supply queue containing that market. `--cap` is expressed in raw asset base units. + When the multisig can authorize the child invocation directly, submit and accept through the CLI: ```sh @@ -430,6 +454,14 @@ tmplr-soroban-vault governance submit-set-allocators \ tmplr-soroban-vault governance submit-set-allowed-adapters \ --admin GCURATOR_OR_MULTISIG... \ --adapters CBLENDADAPTER...,CCUSTODIALADAPTER... +tmplr-soroban-vault governance submit-set-cap \ + --admin GCURATOR_OR_MULTISIG... \ + --market-id 0 \ + --cap 1000000000 +tmplr-soroban-vault governance submit-set-cap \ + --admin GCURATOR_OR_MULTISIG... \ + --market-id 1 \ + --cap 1000000000 tmplr-soroban-vault governance submit-set-supply-queue \ --admin GCURATOR_OR_MULTISIG... \ --entry 0:CBLENDADAPTER... \ @@ -456,12 +488,18 @@ stellar contract invoke \ --paused true ``` +Run `curator refresh-markets` after adapter NAV changes and before relying on share-rate or +accounting views. `curator allocate-supply` observes adapter `total_assets` after supplying, but +`curator allocate-withdraw` verifies the realized token balance delta and subtracts that amount from +stored principal; it does not refresh route NAV. + For custodial adapters, use `deploy adapters --custodian
` to append custodial routes, -then allow the deployed adapter and add it to the supply queue before allocating to it. Each -custodial adapter is bound to the manifest asset token at deployment and rejects calls for any -other asset. The custodian, adapter admin, or vault can explicitly report route NAV on the adapter. -Reports include the current stored NAV and a monotonically increasing nonce so stale heartbeats -cannot re-add assets that have already been released back to the vault: +then allow the deployed adapter, set a nonzero market cap, refresh reported NAV, and add it to the +supply queue before allocating to it. Each custodial adapter is bound to the manifest asset token at +deployment and rejects calls for any other asset. The custodian, adapter admin, or vault can +explicitly report route NAV on the adapter. Reports include the current stored NAV and a +monotonically increasing nonce so stale heartbeats cannot re-add assets that have already been +released back to the vault: ```sh stellar contract invoke \ @@ -573,7 +611,7 @@ tmplr-soroban-vault curator allocate-supply \ # Allocator recovery from an in-flight withdrawing state. tmplr-soroban-vault curator abort-withdrawing --caller G... --op-id 42 -# Curator maintenance operations. +# Curator maintenance operations. Refresh adapter NAV before relying on share-rate or accounting views. tmplr-soroban-vault curator refresh-markets --caller G... --markets 0,1 tmplr-soroban-vault curator refresh-fees tmplr-soroban-vault curator resync-idle @@ -583,6 +621,12 @@ tmplr-soroban-vault curator set-supply-queue \ --admin G... \ --entry 0:C... +# Fresh markets need a nonzero raw asset-unit cap before governance accepts them in the supply queue. +tmplr-soroban-vault governance submit-set-cap \ + --admin G... \ + --market-id 0 \ + --cap 1000000000 + # Submit the same typed supply queue directly to governance. tmplr-soroban-vault governance submit-set-supply-queue \ --admin G... \ From bee807be3582a5eb7e24e8b85ae5ef32e75b5261 Mon Sep 17 00:00:00 2001 From: carrion256 Date: Wed, 24 Jun 2026 12:12:35 +0200 Subject: [PATCH 09/11] ENG-162 address Kani review feedback --- .github/workflows/kani.yml | 16 +++---- contract/vault/kernel/src/lib.rs | 43 +++++++++++++++---- contract/vault/kernel/tests/property_tests.rs | 5 +++ tools/soroban-vault-cli/README.md | 9 ++++ 4 files changed, 57 insertions(+), 16 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 8b90df165..83ba9ad9b 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -42,7 +42,7 @@ jobs: persist-credentials: false - name: Run Universal Account Kani proofs - uses: model-checking/kani-github-action@v1 + uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 with: kani-version: ${{ env.KANI_VERSION }} command: cargo-kani @@ -59,7 +59,7 @@ jobs: persist-credentials: false - name: Run Vault Kernel Kani proofs - uses: model-checking/kani-github-action@v1 + uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 with: kani-version: ${{ env.KANI_VERSION }} command: cargo-kani @@ -76,7 +76,7 @@ jobs: persist-credentials: false - name: Run Vault Kernel external sync immutability Kani proof - uses: model-checking/kani-github-action@v1 + uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 with: kani-version: ${{ env.KANI_VERSION }} command: cargo-kani @@ -99,7 +99,7 @@ jobs: persist-credentials: false - name: Run Vault Kernel withdraw escrow Kani proof - uses: model-checking/kani-github-action@v1 + uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 with: kani-version: ${{ env.KANI_VERSION }} command: cargo-kani @@ -118,7 +118,7 @@ jobs: persist-credentials: false - name: Run Vault Kernel allocation lifecycle Kani proofs - uses: model-checking/kani-github-action@v1 + uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 with: kani-version: ${{ env.KANI_VERSION }} command: cargo-kani @@ -140,7 +140,7 @@ jobs: persist-credentials: false - name: Run Vault Kernel refresh lifecycle Kani proofs - uses: model-checking/kani-github-action@v1 + uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 with: kani-version: ${{ env.KANI_VERSION }} command: cargo-kani @@ -160,7 +160,7 @@ jobs: persist-credentials: false - name: Run Vault Kernel emergency recovery Kani proofs - uses: model-checking/kani-github-action@v1 + uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 with: kani-version: ${{ env.KANI_VERSION }} command: cargo-kani @@ -183,7 +183,7 @@ jobs: persist-credentials: false - name: Run Vault Kernel refresh fee Kani proofs - uses: model-checking/kani-github-action@v1 + uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 with: kani-version: ${{ env.KANI_VERSION }} command: cargo-kani diff --git a/contract/vault/kernel/src/lib.rs b/contract/vault/kernel/src/lib.rs index 6662d9919..2e1a6a01d 100644 --- a/contract/vault/kernel/src/lib.rs +++ b/contract/vault/kernel/src/lib.rs @@ -139,11 +139,38 @@ mod kani_proofs { } fn assert_address_eq(left: Address, right: Address) { - let mut index = 0usize; - while index < 32 { - assert_eq!(left.0[index], right.0[index]); - index += 1; - } + assert_eq!(left.0[0], right.0[0]); + assert_eq!(left.0[1], right.0[1]); + assert_eq!(left.0[2], right.0[2]); + assert_eq!(left.0[3], right.0[3]); + assert_eq!(left.0[4], right.0[4]); + assert_eq!(left.0[5], right.0[5]); + assert_eq!(left.0[6], right.0[6]); + assert_eq!(left.0[7], right.0[7]); + assert_eq!(left.0[8], right.0[8]); + assert_eq!(left.0[9], right.0[9]); + assert_eq!(left.0[10], right.0[10]); + assert_eq!(left.0[11], right.0[11]); + assert_eq!(left.0[12], right.0[12]); + assert_eq!(left.0[13], right.0[13]); + assert_eq!(left.0[14], right.0[14]); + assert_eq!(left.0[15], right.0[15]); + assert_eq!(left.0[16], right.0[16]); + assert_eq!(left.0[17], right.0[17]); + assert_eq!(left.0[18], right.0[18]); + assert_eq!(left.0[19], right.0[19]); + assert_eq!(left.0[20], right.0[20]); + assert_eq!(left.0[21], right.0[21]); + assert_eq!(left.0[22], right.0[22]); + assert_eq!(left.0[23], right.0[23]); + assert_eq!(left.0[24], right.0[24]); + assert_eq!(left.0[25], right.0[25]); + assert_eq!(left.0[26], right.0[26]); + assert_eq!(left.0[27], right.0[27]); + assert_eq!(left.0[28], right.0[28]); + assert_eq!(left.0[29], right.0[29]); + assert_eq!(left.0[30], right.0[30]); + assert_eq!(left.0[31], right.0[31]); } fn bounded_state() -> VaultState { @@ -210,7 +237,7 @@ mod kani_proofs { fn assert_refund_owner_is_owner(refund_owner: Option
) { match refund_owner { - Some(owner) => assert_eq!(owner.0[0], OWNER.0[0]), + Some(owner) => assert_address_eq(owner, OWNER), None => panic!("expected refund owner"), } } @@ -1430,8 +1457,8 @@ mod kani_proofs { assert_eq!(withdraw.index, 1); assert_eq!(withdraw.remaining, 2); assert_eq!(withdraw.collected, 2); - assert_eq!(withdraw.owner.0[0], OWNER.0[0]); - assert_eq!(withdraw.receiver.0[0], RECEIVER.0[0]); + assert_address_eq(withdraw.owner, OWNER); + assert_address_eq(withdraw.receiver, RECEIVER); assert_eq!(withdraw.escrow_shares, 3); } else { panic!("sync must preserve withdrawing operation"); diff --git a/contract/vault/kernel/tests/property_tests.rs b/contract/vault/kernel/tests/property_tests.rs index 82da114e8..fe28bdae0 100644 --- a/contract/vault/kernel/tests/property_tests.rs +++ b/contract/vault/kernel/tests/property_tests.rs @@ -1678,6 +1678,11 @@ proptest! { }, ); + if previewed_assets > old_state.idle_assets { + prop_assert!(result.is_err(), "atomic redeem over idle cap succeeded"); + return Ok(()); + } + if let Ok(result) = result { let burned_shares = result .effects diff --git a/tools/soroban-vault-cli/README.md b/tools/soroban-vault-cli/README.md index 420ca9710..8ebb0a165 100644 --- a/tools/soroban-vault-cli/README.md +++ b/tools/soroban-vault-cli/README.md @@ -162,6 +162,9 @@ adapter set, sets a nonzero market cap, and binds it into the supply queue: tmplr-soroban-vault governance submit-set-allowed-adapters \ --admin GCURATOR_OR_MULTISIG... \ --adapters CBLENDADAPTER...,CCUSTODIALADAPTER... +tmplr-soroban-vault governance accept-ready \ + --admin GCURATOR_OR_MULTISIG... \ + --kind allowed-adapters tmplr-soroban-vault governance submit-set-cap \ --admin GCURATOR_OR_MULTISIG... \ @@ -171,11 +174,17 @@ tmplr-soroban-vault governance submit-set-cap \ --admin GCURATOR_OR_MULTISIG... \ --market-id 1 \ --cap 1000000000 +tmplr-soroban-vault governance accept-ready \ + --admin GCURATOR_OR_MULTISIG... \ + --kind cap tmplr-soroban-vault governance submit-set-supply-queue \ --admin GCURATOR_OR_MULTISIG... \ --entry 0:CBLENDADAPTER... \ --entry 1:CCUSTODIALADAPTER... +tmplr-soroban-vault governance accept-ready \ + --admin GCURATOR_OR_MULTISIG... \ + --kind supply-queue ``` Each `--entry` is `market_id:adapter_address`. The `market_id` is the same value passed later to From 919c814d645dc71f087f31c084fe0f8812266298 Mon Sep 17 00:00:00 2001 From: carrion256 Date: Wed, 24 Jun 2026 12:24:08 +0200 Subject: [PATCH 10/11] ENG-162 tighten Kani review coverage --- contract/vault/kernel/src/lib.rs | 20 ++++++- universal-account/src/authentication/mod.rs | 10 +--- universal-account/src/state/migration.rs | 60 ++++++++++++--------- 3 files changed, 54 insertions(+), 36 deletions(-) diff --git a/contract/vault/kernel/src/lib.rs b/contract/vault/kernel/src/lib.rs index 2e1a6a01d..beed8e1b2 100644 --- a/contract/vault/kernel/src/lib.rs +++ b/contract/vault/kernel/src/lib.rs @@ -1216,9 +1216,17 @@ mod kani_proofs { external, TimestampNs::ZERO, ); + let request_id = enqueue_withdrawal( + &mut state, + OWNER, + RECEIVER, + escrow_shares, + collected + remaining, + TimestampNs::ZERO, + ); state.op_state = OpState::Withdrawing(WithdrawingState { op_id, - request_id: 0, + request_id, index: 0, remaining, collected, @@ -1264,9 +1272,17 @@ mod kani_proofs { external, TimestampNs::ZERO, ); + let request_id = enqueue_withdrawal( + &mut state, + OWNER, + RECEIVER, + escrow_shares, + amount, + TimestampNs::ZERO, + ); state.op_state = OpState::Payout(PayoutState { op_id, - request_id: 0, + request_id, receiver: RECEIVER, amount, owner: OWNER, diff --git a/universal-account/src/authentication/mod.rs b/universal-account/src/authentication/mod.rs index 8d6b8569a..c86130f87 100644 --- a/universal-account/src/authentication/mod.rs +++ b/universal-account/src/authentication/mod.rs @@ -207,10 +207,7 @@ pub trait HashForSigning { mod kani_proofs { use near_sdk::{json_types::U64, AccountId}; - use crate::{ - authentication::{ed25519::raw, with_raw_string::WithRawString}, - encoding, PayloadExecutionParameters, - }; + use crate::{authentication::ed25519::raw, encoding, PayloadExecutionParameters}; use super::*; @@ -230,10 +227,7 @@ mod kani_proofs { } fn valid_raw_message(payload: u8) -> MessageWithValidSignature> { - let message = raw::Message::new(WithRawString { - raw: String::new(), - parsed: Payload::new(execution_parameters(), payload), - }); + let message = raw::Message::from_parsed(Payload::new(execution_parameters(), payload)); MessageWithValidSignature(MessageWithSignature { message, diff --git a/universal-account/src/state/migration.rs b/universal-account/src/state/migration.rs index 40fda64bb..f735180ef 100644 --- a/universal-account/src/state/migration.rs +++ b/universal-account/src/state/migration.rs @@ -124,24 +124,24 @@ mod tests { let passkey = p256::SecretKey::from_bytes(&[0x88_u8; 32].into()).unwrap(); - old.keys.insert( - KeyId::Passkey(passkey::VerifyKey(passkey.public_key().into())), - KeyParameters { - block_height: 1111.into(), - index: 2222.into(), - nonce: 3333.into(), - }, - ); - old.keys.insert( - KeyId::Ed25519Raw(raw::VerifyKey([0xee_u8; 32].into())), - KeyParameters { - block_height: 4444.into(), - index: 5555.into(), - nonce: 6666.into(), - }, - ); + let passkey_key = KeyId::Passkey(passkey::VerifyKey(passkey.public_key().into())); + let passkey_parameters = KeyParameters { + block_height: 1111.into(), + index: 2222.into(), + nonce: 3333.into(), + }; + let raw_key = KeyId::Ed25519Raw(raw::VerifyKey([0xee_u8; 32].into())); + let raw_parameters = KeyParameters { + block_height: 4444.into(), + index: 5555.into(), + nonce: 6666.into(), + }; + + old.keys.insert(passkey_key.clone(), passkey_parameters); + old.keys.insert(raw_key.clone(), raw_parameters); env::state_write(&old); + drop(old); let migration = V0 { chain_id: 1234.into(), @@ -153,12 +153,16 @@ mod tests { assert_eq!(new.chain_id, 1234); assert_eq!(new.next_key_index, 42); assert_eq!(new.keys.len(), 2); + assert_eq!(new.keys.get(&passkey_key), Some(&passkey_parameters)); + assert_eq!(new.keys.get(&raw_key), Some(&raw_parameters)); - env::state_write(&state::V1 { + let v1_state = state::V1 { next_key_index: new.next_key_index, keys: new.keys, chain_id: new.chain_id, - }); + }; + env::state_write(&v1_state); + drop(v1_state); let new = V1.run().unwrap(); @@ -166,6 +170,8 @@ mod tests { assert_eq!(new.chain_id, 1234); assert_eq!(new.next_key_index, 42); assert_eq!(new.keys.len(), 2); + assert_eq!(new.keys.get(&passkey_key), Some(&passkey_parameters)); + assert_eq!(new.keys.get(&raw_key), Some(&raw_parameters)); } #[test] @@ -178,16 +184,17 @@ mod tests { chain_id: 1234, }; - old.keys.insert( - KeyId::Ed25519Raw(raw::VerifyKey([0xee_u8; 32].into())), - KeyParameters { - block_height: 4444.into(), - index: 5555.into(), - nonce: 6666.into(), - }, - ); + let raw_key = KeyId::Ed25519Raw(raw::VerifyKey([0xee_u8; 32].into())); + let raw_parameters = KeyParameters { + block_height: 4444.into(), + index: 5555.into(), + nonce: 6666.into(), + }; + + old.keys.insert(raw_key.clone(), raw_parameters); env::state_write(&old); + drop(old); write_state_version(0); let new = UnbrickV1.run().unwrap(); @@ -196,6 +203,7 @@ mod tests { assert_eq!(new.chain_id, 1234); assert_eq!(new.next_key_index, 42); assert_eq!(new.keys.len(), 1); + assert_eq!(new.keys.get(&raw_key), Some(&raw_parameters)); } } From a39c949659c51bb2894f5bded9bdc8b36ac2a106 Mon Sep 17 00:00:00 2001 From: carrion256 Date: Wed, 24 Jun 2026 15:31:28 +0200 Subject: [PATCH 11/11] ENG-162 address Kani CI and CLI review notes --- .github/workflows/kani.yml | 5 ++++- tools/soroban-vault-cli/README.md | 26 +++++++++++++++++++++----- 2 files changed, 25 insertions(+), 6 deletions(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 83ba9ad9b..bebf334fe 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -75,7 +75,7 @@ jobs: with: persist-credentials: false - - name: Run Vault Kernel external sync immutability Kani proof + - name: Run Vault Kernel external sync immutability Kani proofs uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 with: kani-version: ${{ env.KANI_VERSION }} @@ -83,6 +83,9 @@ jobs: args: >- -p templar-vault-kernel --features action-sync-external + --harness rebalance_withdraw_conserves_total_assets_and_moves_external_to_idle + --harness sync_external_assets_preserves_total_as_idle_plus_external + --harness bounded_sync_then_rebalance_conserves_accounting_across_actions --harness sync_external_assets_allocating_only_mutates_external_and_total_assets --harness sync_external_assets_withdrawing_preserves_share_supply_queue_and_actor_fields --harness sync_external_assets_refreshing_only_mutates_external_and_total_assets diff --git a/tools/soroban-vault-cli/README.md b/tools/soroban-vault-cli/README.md index 8ebb0a165..2aef4e859 100644 --- a/tools/soroban-vault-cli/README.md +++ b/tools/soroban-vault-cli/README.md @@ -174,9 +174,15 @@ tmplr-soroban-vault governance submit-set-cap \ --admin GCURATOR_OR_MULTISIG... \ --market-id 1 \ --cap 1000000000 -tmplr-soroban-vault governance accept-ready \ +# After the cap proposals are ready, verify and accept the specific SetCap proposal ids. +tmplr-soroban-vault governance explain --proposal-id CAP_MARKET_0_PROPOSAL_ID +tmplr-soroban-vault governance explain --proposal-id CAP_MARKET_1_PROPOSAL_ID +tmplr-soroban-vault governance accept \ + --admin GCURATOR_OR_MULTISIG... \ + --proposal-id CAP_MARKET_0_PROPOSAL_ID +tmplr-soroban-vault governance accept \ --admin GCURATOR_OR_MULTISIG... \ - --kind cap + --proposal-id CAP_MARKET_1_PROPOSAL_ID tmplr-soroban-vault governance submit-set-supply-queue \ --admin GCURATOR_OR_MULTISIG... \ @@ -270,7 +276,9 @@ Curator commands fall into three groups: For timelocked deployments, submit commands create proposals and `accept-ready` accepts them only after the relevant timelock has elapsed. Use `governance queue` and `governance explain` to inspect -pending proposal ids and readiness. +pending proposal ids and readiness. For market caps, prefer accepting the specific SetCap proposal id +after `explain` confirms the market id; avoid filtering ready proposals by cap kind because that +text match can also include cap-group proposals. ### Single Curator @@ -292,7 +300,11 @@ tmplr-soroban-vault governance submit-set-cap \ --admin GCURATOR... \ --market-id 0 \ --cap 1000000000 -tmplr-soroban-vault governance accept-ready --admin GCURATOR... --kind cap +# After the cap proposal is ready, verify and accept the specific SetCap proposal id. +tmplr-soroban-vault governance explain --proposal-id CAP_MARKET_0_PROPOSAL_ID +tmplr-soroban-vault governance accept \ + --admin GCURATOR... \ + --proposal-id CAP_MARKET_0_PROPOSAL_ID tmplr-soroban-vault governance submit-set-supply-queue \ --admin GCURATOR... \ @@ -318,7 +330,11 @@ tmplr-soroban-vault governance submit-set-cap \ --admin GCURATOR... \ --market-id 0 \ --cap 1000000000 -tmplr-soroban-vault governance accept-ready --admin GCURATOR... --kind cap +# After the cap proposal is ready, verify and accept the specific SetCap proposal id. +tmplr-soroban-vault governance explain --proposal-id CAP_MARKET_0_PROPOSAL_ID +tmplr-soroban-vault governance accept \ + --admin GCURATOR... \ + --proposal-id CAP_MARKET_0_PROPOSAL_ID tmplr-soroban-vault curator set-supply-queue \ --admin GCURATOR... \ --entry 0:CBLENDADAPTER... \