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

[DSOTec]

Problem

stellar/stealth-vault shipped in Wave 6 as a time-locked deposit primitive but
never got the hardening pass that stealth-sender and wraith-names received.
It is the last core contract that custodies user funds and it had:

• no admin and no pause switch — no way to stop new deposits during an incident;
• no reentrancy analysis doc and no AUDIT_SUMMARY.md;
• no gas bench coverage, so its write paths were invisible to the CI gas gate;
• no machine-checked time-lock invariants;
• GRACE_PERIOD = 1000 hard-coded, changeable only by redeploying;
• only the depositor able to refund, so a lost key stranded funds forever.

Two live defects surfaced while wiring the benches and the real announcer:

1. deposit announced under scheme_id = 1, but stealth-announcer
   asserts scheme_id == STELLAR_V2_SCHEME_ID (2). Every deposit against the
   production announcer would have panicked. The unit tests registered a
   permissive mock announcer, so nothing caught it.
2. The refund-window check could wrap. refund_after <= unlock_ledger + GRACE_PERIOD
   is a wrapping add under the workspace release profile (overflow-checks = false),
   so an unlock_ledger near u32::MAX admitted a window the validation was
   meant to reject.

Solution

Admin + pause (src/lib.rs)

• init(admin, announcer) records a pause admin and seeds the grace period.
• pause / unpause / is_paused / admin, mirroring the sender's and names'
  admin-panic pattern so the posture is uniform across contracts.
• Only deposit is guarded. claim, refund, and refund_permissionless stay
  callable while paused — parity with the sender's withdraw_many exception, so
  an admin can never trap user funds.

Permissionless refund

• refund_permissionless(caller, deposit_id) opens one grace period after
  refund_after. Funds always route to the recorded depositor; caller only
  pays the fee and is authorised so the invocation is attributable. It emits the
  same refund event and refund_count metric as the depositor path, so
  indexers need no change.

Configurable grace period

• Seeded at init from DEFAULT_GRACE_PERIOD, retunable by the admin via
  set_grace_period (rejects zero). Reads fall back to the default, so vaults
  deployed before the key existed keep working.

Defect fixes

• ANNOUNCE_SCHEME_ID = 2, with tests/announcer.rs wiring the real
  stealth-announcer so the two cannot drift again.
• Both window computations use saturating_add.

Kani proofs (src/proofs/mod.rs, src/mock_sdk.rs)

• (a) proof_claim_before_unlock_always_errors
• (b) proof_refund_before_refund_after_always_errors
• (c) proof_claim_and_refund_are_mutually_exclusive
• plus proof_permissionless_window_never_precedes_refund_after, anchoring the
  saturating arithmetic (b) leans on.

They run against the real claim / refund / refund_permissionless
bodies, compiled against a hand-rolled mock_sdk in place of soroban-sdk —
the same cfg(kani) pattern stealth-registry already uses. The harness is
zero-sized and heap-free (state in one static, fixed-capacity slot arrays) so
CBMC stays well inside the CI budget. stellar/stealth-vault is added to the
existing stellar-kani job.

Metrics — deposit_count, deposit_volume, claim_count, refund_count
were wired in #171; this PR adds the permissionless path's refund_count and
pins all four in stellar/METRICS.md's per-contract table.

Docs — new stellar/stealth-vault/AUDIT_SUMMARY.md mirroring the sender's,
covering the deposit-id derivation (including the ephemeral-key-reuse collision
case) and an explicit no reentrancy guard required section grounded in the
single-invocation Soroban model. Linked from stellar/README.md.

Testing

cargo test -p stealth-vault     # 29 passed (27 unit + 2 integration)
cargo kani --package stealth-vault
cargo fmt --all --check         # clean
cargo bench -p wraith-stellar-bench --bench gas

New coverage: admin/init (5), pause (6), permissionless refund (4), metric shape
for the permissionless path (1), real-announcer integration (2).

The four new bench rows are new ops, so bench/compare.py reports them under
"new ops (no baseline gate)" and the +5% PR gate is unaffected. PERF.md's
auto-managed block was regenerated with bench/update_perf_md.py; CI refreshes
it again on the next develop push.

Notes for reviewers

• init gains an admin parameter — an ABI break. The vault is not in
  deploy.sh, contract-ids.json, or abi/, so nothing in-repo depends on the
  old signature.
• refund's signature is unchanged; the permissionless path is a new
  entrypoint rather than a change to the existing one.
• set_grace_period moves the permissionless window for deposits already in
  flight (it is computed at call time). That is deliberate — it is the lever an
  admin needs — and proof (b) shows it can never bring the window forward past
  refund_after.

Closes #156

[drips-wave]

@DSOTec Great news! 🎉 Based on an automated assessment of this PR, the linked Wave issue(s) no longer count against your application limits.

You can now already apply to more issues while waiting for a review of this PR. Keep up the great work! 🚀

Learn more about application limits

[truthixify]

Merged. Pause guards with claim and refund still callable while paused, permissionless refund after grace, and a snapshot per path. The mock_sdk split keeps the proofs readable too. Strong work @DSOTec, second substantial contracts PR from you this wave.