Kani proofs for stealth-sender: fee arithmetic + send atomicity

[truthixify]

Tier: M (2-4 days) | Type: security

Context. Wave 7 shipped Kani for stealth-registry (three invariants at stealth-registry/src/proofs/mod.rs). stealth-sender is the higher-value target (it holds user funds and does raw i128 fee arithmetic with fee_bp up to 50) and has none. Property tests exist at stealth-sender/tests/properties.rs but only sample; Kani would prove the fee bounds hold across the full input space.

Scope.

• New stealth-sender/src/proofs/mod.rs gated by #[cfg(kani)].
• Prove: (a) fee = amount * fee_bp / 10_000 never overflows i128 for any positive amount and fee_bp <= 50, (b) net_to_recipient + fee_to_recipient == amount for every send that reaches token-transfer, (c) withdraw_many cannot leave the contract in a state where sum(unclaimed) > sum(deposited).
• Reuse stealth-registry/src/mock_sdk.rs shape.
• Extend the existing stellar-kani CI job to include the sender crate.
• Document the proofs' claim + non-goal in a new stellar/stealth-sender/PROOFS.md.

Acceptance.

• Three named proofs pass in the stellar-kani job in under 5 minutes wall clock
• A deliberately broken change to fee arithmetic (mutation test) fails the job
• stellar/stealth-sender/PROOFS.md documents each proof's claim + non-goal
• stellar/stealth-sender/README.md cross-links to PROOFS.md

Files. stellar/stealth-sender/src/proofs/mod.rs (new), stellar/stealth-sender/src/mock_sdk.rs (new), stellar/stealth-sender/PROOFS.md (new), stellar/stealth-sender/README.md, .github/workflows/ci.yml.

[sudo-robi]

@sudo-robi has applied to work on this issue as part of the Stellar Wave Program's 8th wave.

Hi maintainer I'm a full stack developer and smart contract developer and auditor let me help you resolve this issue and I assure you it will be thoroughly done neatly as I have seen my way to solve the issue.

ℹ️ Repo Maintainers: To accept this application, review their application or assign @sudo-robi to this issue.

[Bouynaty]

@Bouynaty has applied to work on this issue as part of the Stellar Wave Program's 8th wave.

Hello, I’m eager to contribute to the project and would really appreciate the chance to tackle this issue. Thanks for considering me!

ℹ️ Repo Maintainers: To accept this application, review their application or assign @Bouynaty to this issue.

[Regina-uriel]

@Regina-uriel has applied to work on this issue as part of the Stellar Wave Program's 8th wave.

Can I work on this issue?

ℹ️ Repo Maintainers: To accept this application, review their application or assign @Regina-uriel to this issue.

[thebabalola]

@thebabalola has applied to work on this issue as part of the Stellar Wave Program's 8th wave.

Hi maintainer, I've worked with Rust testing at this level before — chaos harnesses are where real contract bugs surface. Extending coverage to vault, splitter, and governance flows, I'd target fee arithmetic edge cases, boundary conditions, and failure-path atomicity. Each discovered issue gets a minimal repro before the fix. I'll match your existing harness conventions exactly. Ready to dive in once assigned!

ℹ️ Repo Maintainers: To accept this application, review their application or assign @thebabalola to this issue.

[oscar24357]

@oscar24357 has applied to work on this issue as part of the Stellar Wave Program's 8th wave.

hello boss, good afternoon, can you please assign this issue to me.

ℹ️ Repo Maintainers: To accept this application, review their application or assign @oscar24357 to this issue.

[stpatrickghost]

@stpatrickghost has applied to work on this issue as part of the Stellar Wave Program's 8th wave.

Can I work on this?

ℹ️ Repo Maintainers: To accept this application, review their application or assign @stpatrickghost to this issue.

[penielgold-hub]

@penielgold-hub has applied to work on this issue as part of the Stellar Wave Program's 8th wave.

Hello maintainer, I would like to work on this issue

ℹ️ Repo Maintainers: To accept this application, review their application or assign @penielgold-hub to this issue.