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.

[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.

[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.

[TS-mfon]

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

GM

i'm a blockchain developer

please can i work on this issue

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