feat(stellar): production-harden stealth-vault (admin, pause, Kani proofs, benches, audit doc)

.github/workflows/ci.yml

@@ -179,6 +179,11 @@ jobs:
         with:
           working-directory: stellar/stealth-registry
 
+      - name: Verify stealth-vault invariants with Kani
+        uses: model-checking/kani-github-action@v1
+        with:
+          working-directory: stellar/stealth-vault
+
   stellar-nightly:
     if: github.event_name == 'schedule' && github.event.schedule == '23 4 * * *'
     runs-on: ubuntu-latest

stellar/METRICS.md

@@ -186,8 +186,13 @@ That is negligible on a write path but material on a cheap read path:
 
 `resolve` exceeds the CI bench gate's +5% per-op threshold, so
 `stellar/bench/baseline.json` was rotated alongside the wiring. No other benched
-op moved: the splitter, vault, and governance write paths are not in the gas
-bench, and every other measured op is byte-identical.
+op moved: the splitter and governance write paths are not in the gas bench, and
+every other measured op is byte-identical.
+
+The vault's four metrics are benched — see the `stealth-vault` rows in
+[PERF.md](./PERF.md). All four sit on write paths, so at the ~4,164-instruction
+fixed cost above the emissions are roughly 2% of `claim` / `refund` and 3% of
+`deposit` (which emits two).
 
 Instrument cheap read paths deliberately — the fixed emission cost dominates
 them.

stellar/MIGRATION_V0_TO_V1.md

@@ -118,9 +118,13 @@ Cutting v1 contracts expands contract state to support persistent rent isolation
 ### 2.5 `stealth-vault`
 - **v0 Storage Layout:** N/A (New in v1).
 - **v1 Storage Layout:**
-  - Storage Type: `instance()` for `Announcer` address; `persistent()` for deposit records.
+  - Storage Type: `instance()` for `Announcer` address, admin, and pause state;
+    `persistent()` for deposit records.
   - DataKeys:
     - `DataKey::Announcer` -> `Address`
+    - `DataKey::Admin` -> `Address` (pause admin; set at `init`)
+    - `DataKey::Paused` -> `bool` (blocks new deposits; exits stay callable)
+    - `DataKey::GracePeriod` -> `u32` (ledgers; defaults to 1000, admin-retunable)
     - `DataKey::Deposit(BytesN<32>)` -> `DepositEntry`:
       - `sender`: `Address`
       - `recipient`: `Address`

stellar/PAUSE.md

@@ -17,6 +17,7 @@ data: `(caller,)`).
 | stealth-registry   | No        | Not implemented; non-custodial metadata writes, registrations are not guarded |
 | stealth-sender     | Yes       | Moves tokens; pause prevents sends during incident |
 | wraith-names       | Yes       | Name registry with ownership; pause prevents registrations, updates, releases, and TTL extensions |
+| stealth-vault      | Yes       | Custodies time-locked deposits; pause prevents new deposits during an incident |
 
 ## Guarded Surface
 
@@ -29,6 +30,18 @@ Guarded by `require_not_paused`:
 NOT guarded (users must be able to exit during an incident):
 - `withdraw_many` — batch asset exits
 
+### stealth-vault
+
+Guarded by `require_not_paused`:
+- `deposit` — token transfer into the vault + announcement
+
+NOT guarded (users must be able to exit during an incident):
+- `claim` — recipient takes an unlocked deposit
+- `refund` — depositor reclaims an unclaimed deposit after `refund_after`
+- `refund_permissionless` — anyone returns a deposit to its depositor one grace
+  period after `refund_after`
+- `get_deposit`, `is_paused`, `admin`, `grace_period` — read-only accessors
+
 ### wraith-names
 
 Guarded by `require_not_paused`:
@@ -44,7 +57,8 @@ NOT guarded (read-only lookups remain available):
 ## Usage
 ```rust
 // Admin initialises the pause capability
-client.init(&admin);  // wraith-names only; stealth-sender admin set in init()
+client.init(&admin);  // wraith-names only; stealth-sender and stealth-vault
+                      // take the admin as an init() argument
 
 // Pause
 client.pause(&admin);

stellar/PERF.md

@@ -68,7 +68,7 @@ ownership checks.
 ## Current Numbers
 
 <!-- BENCH:CURRENT:START -->
-These are the harness results auto-updated from `develop` (measured 2026-08-26, commit `233c055dcee3`).
+These are the harness results auto-updated from `develop` (measured 2026-08-26, commit `28634256692c`).
 
 | Contract | Function | Parameters | Instructions | Mem bytes | Read entries | Write entries | Read bytes | Write bytes | Event bytes |
 |---|---|---:|---:|---:|---:|---:|---:|---:|---:|
@@ -91,6 +91,11 @@ These are the harness results auto-updated from `develop` (measured 2026-08-26,
 | wraith-names | resolve | miss | 27723 | 2655 | 2 | 0 | 104 | 0 | 0 |
 | wraith-names | name_of | hit | 49222 | 4865 | 3 | 0 | 604 | 0 | 0 |
 | wraith-names | name_of | miss | 25374 | 2127 | 2 | 0 | 104 | 0 | 0 |
+| stealth-vault | deposit | asset=xlm | 262123 | 39207 | 6 | 4 | 1228 | 924 | 1084 |
+| stealth-vault | deposit | asset=issued | 261883 | 39207 | 6 | 4 | 1228 | 924 | 1084 |
+| stealth-vault | claim | unlocked | 201891 | 32853 | 4 | 4 | 1476 | 520 | 628 |
+| stealth-vault | refund | depositor | 197513 | 30286 | 3 | 4 | 1608 | 520 | 628 |
+| stealth-vault | refund_permissionless | keeper | 210287 | 32111 | 3 | 4 | 1608 | 520 | 628 |
 <!-- BENCH:CURRENT:END -->
 
 ## Gas Regression Gate

stellar/README.md

@@ -36,6 +36,27 @@ To run tests for all contracts:
 cargo test
 ```
 
+## Audits & Formal Verification
+
+Per-contract audit write-ups for the contracts that custody user funds:
+
+- [stealth-sender/AUDIT_SUMMARY.md](./stealth-sender/AUDIT_SUMMARY.md) — atomic
+  transfer + announcement coupling, SAC compatibility, batch atomicity.
+- [stealth-vault/AUDIT_SUMMARY.md](./stealth-vault/AUDIT_SUMMARY.md) — deposit-id
+  derivation, the single-invocation Soroban model and why no reentrancy guard is
+  required, and the Kani time-lock proofs.
+
+Machine-checked invariants live alongside the contracts they cover and run in the
+`stellar-kani` CI job:
+
+```bash
+cargo kani --package stealth-registry
+cargo kani --package stealth-vault
+```
+
+Cross-cutting posture docs: [PAUSE.md](./PAUSE.md), [METRICS.md](./METRICS.md),
+[PERF.md](./PERF.md), [MULTISIG.md](./MULTISIG.md).
+
 ## Deployment
 
 A deployment script is provided to deploy all contracts in one go.

stellar/bench/Cargo.toml

@@ -8,6 +8,7 @@ soroban-sdk = { workspace = true, features = ["testutils"] }
 stealth-announcer = { path = "../stealth-announcer", features = ["testutils"] }
 stealth-registry = { path = "../stealth-registry", features = ["testutils"] }
 stealth-sender = { path = "../stealth-sender", features = ["testutils"] }
+stealth-vault = { path = "../stealth-vault", features = ["testutils"] }
 wraith-names = { path = "../wraith-names", features = ["testutils"] }
 
 [[bench]]

stellar/bench/src/lib.rs

@@ -1,4 +1,4 @@
-use soroban_sdk::testutils::Address as _;
+use soroban_sdk::testutils::{Address as _, Ledger as _};
 use soroban_sdk::token::StellarAssetClient;
 use soroban_sdk::{vec, Address, Bytes, BytesN, Env, String as SorobanString, Vec as SorobanVec};
 
@@ -7,6 +7,7 @@ use stealth_announcer::{
 };
 use stealth_registry::{StealthRegistryContract, StealthRegistryContractClient};
 use stealth_sender::{StealthSenderContract, StealthSenderContractClient};
+use stealth_vault::{StealthVaultContract, StealthVaultContractClient};
 use wraith_names::{WraithNamesContract, WraithNamesContractClient};
 
 #[derive(Clone, Debug)]
@@ -192,6 +193,94 @@ pub fn collect_rows() -> std::vec::Vec<Row> {
         let _ = client.try_name_of(&bytes(env, 64, 8));
     }));
 
+    for asset in ["xlm", "issued"] {
+        rows.push(measure(
+            "stealth-vault",
+            "deposit",
+            format!("asset={asset}"),
+            |env| {
+                env.mock_all_auths();
+                let (client, token, sender, recipient) = vault_with_token(env, asset == "xlm");
+                client.deposit(
+                    &sender,
+                    &recipient,
+                    &1_000,
+                    &token,
+                    &VAULT_UNLOCK_LEDGER,
+                    &VAULT_REFUND_AFTER,
+                    &BytesN::from_array(env, &[11u8; 32]),
+                );
+            },
+        ));
+    }
+
+    rows.push(measure(
+        "stealth-vault",
+        "claim",
+        "unlocked".into(),
+        |env| {
+            env.mock_all_auths();
+            let (client, token, sender, recipient) = vault_with_token(env, true);
+            let deposit_id = client.deposit(
+                &sender,
+                &recipient,
+                &1_000,
+                &token,
+                &VAULT_UNLOCK_LEDGER,
+                &VAULT_REFUND_AFTER,
+                &BytesN::from_array(env, &[12u8; 32]),
+            );
+            env.ledger()
+                .with_mut(|li| li.sequence_number = VAULT_UNLOCK_LEDGER);
+            client.claim(&deposit_id, &recipient);
+        },
+    ));
+
+    rows.push(measure(
+        "stealth-vault",
+        "refund",
+        "depositor".into(),
+        |env| {
+            env.mock_all_auths();
+            let (client, token, sender, recipient) = vault_with_token(env, true);
+            let deposit_id = client.deposit(
+                &sender,
+                &recipient,
+                &1_000,
+                &token,
+                &VAULT_UNLOCK_LEDGER,
+                &VAULT_REFUND_AFTER,
+                &BytesN::from_array(env, &[13u8; 32]),
+            );
+            env.ledger()
+                .with_mut(|li| li.sequence_number = VAULT_REFUND_AFTER);
+            client.refund(&deposit_id);
+        },
+    ));
+
+    rows.push(measure(
+        "stealth-vault",
+        "refund_permissionless",
+        "keeper".into(),
+        |env| {
+            env.mock_all_auths();
+            let (client, token, sender, recipient) = vault_with_token(env, true);
+            let deposit_id = client.deposit(
+                &sender,
+                &recipient,
+                &1_000,
+                &token,
+                &VAULT_UNLOCK_LEDGER,
+                &VAULT_REFUND_AFTER,
+                &BytesN::from_array(env, &[14u8; 32]),
+            );
+            env.ledger().with_mut(|li| {
+                li.sequence_number = VAULT_REFUND_AFTER + stealth_vault::DEFAULT_GRACE_PERIOD
+            });
+            client.refund_permissionless(&Address::generate(env), &deposit_id);
+        },
+    ));
+
     rows
 }
 
@@ -360,6 +449,29 @@ where
     }
 }
 
+/// Vault deposits must clear `unlock_ledger + grace_period`; these constants keep
+/// every vault row on the same window so the numbers stay comparable.
+const VAULT_UNLOCK_LEDGER: u32 = 100;
+const VAULT_REFUND_AFTER: u32 = 2_000;
+
+/// A registered, initialised vault plus a funded sender and a recipient.
+fn vault_with_token(
+    env: &Env,
+    native: bool,
+) -> (
+    StealthVaultContractClient<'static>,
+    Address,
+    Address,
+    Address,
+) {
+    let announcer_id = env.register(StealthAnnouncerContract, ());
+    let vault_id = env.register(StealthVaultContract, ());
+    let client = StealthVaultContractClient::new(env, &vault_id);
+    client.init(&Address::generate(env), &announcer_id);
+    let (token, sender) = funded_token(env, native);
+    (client, token, sender, Address::generate(env))
+}
+
 fn funded_token(env: &Env, native: bool) -> (Address, Address) {
     let admin = Address::generate(env);
     let sender = Address::generate(env);