diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml new file mode 100644 index 000000000..bebf334fe --- /dev/null +++ b/.github/workflows/kani.yml @@ -0,0 +1,197 @@ +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@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 + 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@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 + 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 external sync immutability Kani proofs + uses: model-checking/kani-github-action@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 + with: + kani-version: ${{ env.KANI_VERSION }} + command: cargo-kani + 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 + --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@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 + 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 + 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@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 + 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@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 + 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-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@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 + 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 + 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@2534b7aeb3c6b4b0a5ecc3981bb3e63d47b5b126 + 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 + --harness refresh_fees_active_rates_only_mint_fee_shares_and_update_anchor 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/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) diff --git a/contract/universal-account/tests/universal_account.rs b/contract/universal-account/tests/universal_account.rs index 8108ef119..ff0543467 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 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] +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..fc1761789 100644 --- a/contract/vault/kernel/Cargo.toml +++ b/contract/vault/kernel/Cargo.toml @@ -45,7 +45,6 @@ all-actions = [ "action-allocation-lifecycle", "action-refresh-lifecycle", ] - [dependencies] derive_more.workspace = true primitive-types = { version = "0.14.0", default-features = false } @@ -62,3 +61,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/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 51f40642d..beed8e1b2 100644 --- a/contract/vault/kernel/src/lib.rs +++ b/contract/vault/kernel/src/lib.rs @@ -60,5 +60,1707 @@ pub use transitions::{ withdrawal_collected, withdrawal_settled, withdrawal_step_callback, TransitionError, TransitionRes, TransitionResult, WithdrawalRequest, }; + +#[cfg(kani)] +mod kani_proofs { + use alloc::{vec, vec::Vec}; + + use super::*; + #[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]); + const RECEIVER: Address = Address([0x22; 32]); + 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::(); + kani::assume(amount <= MAX_AMOUNT); + amount + } + + fn nonzero_bounded_amount() -> u128 { + let amount = bounded_amount(); + kani::assume(amount > 0); + amount + } + + 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, + } + } + + #[cfg(feature = "action-refresh-fees")] + fn active_fee_config() -> VaultConfig { + VaultConfig { + fees: FeesSpec::new( + FeeSlot::new(Wad::one() / 10, Address([0x66; 32])), + FeeSlot::zero(), + 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) { + 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 { + 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 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"), + } + } + + fn assert_emit_event_effect(effect: &KernelEffect) { + match effect { + KernelEffect::EmitEvent { .. } => {} + _ => panic!("expected emit event effect"), + } + } + + #[cfg(feature = "action-refresh-fees")] + fn assert_mint_shares_effect(effect: &KernelEffect) -> u128 { + match effect { + KernelEffect::MintShares { shares, .. } => { + assert!(*shares > 0); + *shares + } + _ => panic!("refresh fees must not move assets or non-fee shares"), + } + } + + fn assert_refund_owner_is_owner(refund_owner: Option
) { + match refund_owner { + Some(owner) => assert_address_eq(owner, OWNER), + None => panic!("expected refund owner"), + } + } + + #[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)); + } + + #[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); + } + + #[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() { + 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); + } + + #[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); + } + + #[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); + } + + #[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, + idle, + external, + TimestampNs::ZERO, + ); + 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::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); + } + + #[kani::proof] + #[kani::unwind(40)] + 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(); + let escrow_shares = nonzero_bounded_amount(); + let burn_shares = bounded_amount(); + let amount = bounded_amount(); + kani::assume(burn_shares <= escrow_shares); + kani::assume(amount <= idle); + + let op_id = 42; + 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, + ); + 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 = "action-recovery")] + #[kani::proof] + #[kani::unwind(8)] + fn emergency_reset_allocating_restores_remaining_assets_to_idle() { + let idle = bounded_amount(); + let external = bounded_amount(); + let total_shares = bounded_amount(); + let remaining = bounded_amount(); + let op_id = 51; + + 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!( + 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_withdrawing_restores_collected_assets_and_refunds_escrow() { + let idle = bounded_amount(); + let external = bounded_amount(); + 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, + total_shares, + idle, + 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, + index: 0, + remaining, + collected, + receiver: RECEIVER, + owner: OWNER, + escrow_shares, + }); + + 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); + } + + #[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, + ); + 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, + }); + + 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_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, + before.withdraw_queue.status().length + ); + 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(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_id = 61; + + let mut state = + VaultState::with_initial(idle + external, shares, idle, external, TimestampNs::ZERO); + 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; + 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); + 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); + } + + #[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_address_eq(withdraw.owner, OWNER); + assert_address_eq(withdraw.receiver, RECEIVER); + 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(), + None, + &SELF, + 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"))] + #[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(); + + 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.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, + 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); + } + + #[cfg(feature = "action-refresh-fees")] + #[kani::proof] + #[kani::unwind(8)] + fn refresh_fees_active_rates_only_mint_fee_shares_and_update_anchor() { + let idle = 100u128; + let external = 0u128; + let shares = 100u128; + 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(); + + 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); + 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; 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 { diff --git a/contract/vault/kernel/tests/property_tests.rs b/contract/vault/kernel/tests/property_tests.rs index 29cc91088..fe28bdae0 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,258 @@ 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 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 + .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 +3958,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/tools/soroban-vault-cli/README.md b/tools/soroban-vault-cli/README.md index bd35f2532..2aef4e859 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,17 +156,41 @@ 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 accept-ready \ + --admin GCURATOR_OR_MULTISIG... \ + --kind allowed-adapters + +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 +# 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... \ + --proposal-id CAP_MARKET_1_PROPOSAL_ID 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 @@ -196,8 +220,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 +234,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 @@ -251,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 @@ -269,6 +296,16 @@ 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 +# 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... \ --entry 0:CBLENDADAPTER... @@ -289,6 +326,15 @@ 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 +# 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... \ @@ -312,6 +358,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 +479,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 +513,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 +636,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 +646,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... \ diff --git a/universal-account/src/authentication/mod.rs b/universal-account/src/authentication/mod.rs index 19432cc67..c86130f87 100644 --- a/universal-account/src/authentication/mod.rs +++ b/universal-account/src/authentication/mod.rs @@ -202,3 +202,63 @@ 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, 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::from_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..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,5 +203,67 @@ 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)); + } +} + +#[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); } }